Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/Nominal/Fv.thy
changeset 1216 06ace3a1eedd
parent 1215 aec9576b3950
child 1217 74e2b9b95add 
--- a/Quot/Nominal/Fv.thy	Mon Feb 22 17:19:28 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 18:09:44 2010 +0100
@@ -220,11 +220,11 @@
 ML {*
 fun alpha_inj_tac dist_inj intrs elims =
   SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'
-  rtac @{thm iffI} THEN' RANGE [
+  (rtac @{thm iffI} THEN' RANGE [
      (eresolve_tac elims THEN_ALL_NEW
        asm_full_simp_tac (HOL_ss addsimps dist_inj)
      ),
-     (asm_full_simp_tac (HOL_ss addsimps intrs))]
+     asm_full_simp_tac (HOL_ss addsimps intrs)])
 *}
 
 ML {*
nominal2