# HG changeset patch
# User huffman
# Date 1271380865 25200
# Node ID f84fa49a0b69c82a029ca04ebe35841577c8c438
# Parent  bffb04bf4e8366c0791156c84b84300bd92c3b70
add rule deflation_ID to proof script for take + constructor rules

diff -r bffb04bf4e83 -r f84fa49a0b69 src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Thu Apr 15 21:24:00 2010 +0200
+++ b/src/HOLCF/Domain.thy	Thu Apr 15 18:21:05 2010 -0700
@@ -149,8 +149,8 @@
   cfcomp2 sfst_defined_iff ssnd_defined_iff
 
 lemmas take_con_rules =
-  ID1 ssum_map_sinl' ssum_map_sinr' ssum_map_strict
-  sprod_map_spair' sprod_map_strict u_map_up u_map_strict
+  ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
+  deflation_strict deflation_ID ID1 cfcomp2
 
 use "Tools/cont_consts.ML"
 use "Tools/cont_proc.ML"
diff -r bffb04bf4e83 -r f84fa49a0b69 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Apr 15 21:24:00 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Apr 15 18:21:05 2010 -0700
@@ -184,8 +184,7 @@
       val rhs = con_app2 con one_rhs args;
       val goal = mk_trp (lhs === rhs);
       val rules =
-          [ax_abs_iso]
-          @ @{thms take_con_rules ID1 cfcomp2 deflation_strict}
+          [ax_abs_iso] @ @{thms take_con_rules}
           @ take_Suc_thms @ deflation_thms @ deflation_take_thms;
       val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
     in pg con_appls goal (K tacs) end;