# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269425619 -3600
# Node ID 6ad74d73e1b18af3757b71c7fc3a3b818f338341
# Parent  91ab98dd9999cd1a3400fb43d21ab71164186b65
Support proof modification for Core Haskell.

diff -r 91ab98dd9999 -r 6ad74d73e1b1 Nominal/Fv.thy
--- 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})
 *}