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.
Support proof modification for Core Haskell.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 24 Mar 2010 11:13:39 +0100
changeset 1625 6ad74d73e1b1
parent 1624 91ab98dd9999
child 1626 0d7d0b8adca5
Support proof modification for Core Haskell.
Nominal/Fv.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Fv.thy	Wed Mar 24 10:55:59 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 24 11:13:39 2010 +0100
@@ -1091,8 +1091,11 @@
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric] Collect_disj_eq[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW
   simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
 *}
nominal2