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.
Nominal/Fv.thy
changeset 1487 b55b78e63913
parent 1482 a98c15866300
child 1498 2ff84b1f551f 
--- a/Nominal/Fv.thy	Wed Mar 17 17:09:01 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 17 17:40:14 2010 +0100
@@ -609,10 +609,8 @@
   THEN_ALL_NEW
   split_conjs THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
-  (rtac @{thm alpha_gen_compose_sym} THEN' RANGE [
-    (asm_full_simp_tac (HOL_ss addsimps @{thms plus_perm_eq})),
-    (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
-  ])
+  TRY o (rtac @{thm alpha_gen_compose_sym2} ORELSE' rtac @{thm alpha_gen_compose_sym}) THEN_ALL_NEW
+  (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
 *}
 
 ML {*
nominal2