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 1433 7a9217a7f681
parent 1428 4029105011ca
child 1452 31f000d586bb 
--- a/Nominal/Fv.thy	Thu Mar 11 19:43:50 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 11 20:49:31 2010 +0100
@@ -714,7 +714,7 @@
   simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (
     REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conjs THEN'
     asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]
-      swap_fresh_fresh fresh_atom swap_at_base_simps(3)}))
+      swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh}))
 *}
 
 ML {*
@@ -766,7 +766,7 @@
 ML {*
 fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW (
   rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom finite_insert finite.emptyI finite_Un})
+  asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image finite_insert finite.emptyI finite_Un})
 *}
 
 ML {*
nominal2