Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Wed, 27 Mar 2013 17:23:00 +0000
changeset 3216 bc2c3a1f87ef
parent 3215 3cfd4fc42840
child 3217 d67a6a48f1c7
tuned
Nominal/Nominal2_Base.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Nominal2_Base.thy	Wed Mar 27 16:09:46 2013 +0100
+++ b/Nominal/Nominal2_Base.thy	Wed Mar 27 17:23:00 2013 +0000
@@ -3319,11 +3319,6 @@
   apply (auto simp add: fresh_Pair intro: a)
   done
 
-lemma "1 = 1 &&& 2 = 2"
-apply(tactic {* ALLGOALS (asm_full_simp_tac @{simpset}) *})
-done
-
-
 simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> 'b::pt)") = {* fn _ => fn ss => fn ctrm =>
   let
      val ctxt = Simplifier.the_context ss
nominal2