# HG changeset patch
# User huffman
# Date 1274542240 25200
# Node ID a1656804fcadf3f5bd11a0ff8396201b4e01925e
# Parent  8f9f3d61ca8c20b02302a70be62c9fdb461949b2
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context

diff -r 8f9f3d61ca8c -r a1656804fcad src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Fri May 21 17:16:16 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Sat May 22 08:30:40 2010 -0700
@@ -42,14 +42,13 @@
 
 (************************** miscellaneous functions ***************************)
 
-val simple_ss =
-  HOL_basic_ss addsimps simp_thms;
+val simple_ss = HOL_basic_ss addsimps simp_thms;
 
-val beta_ss =
-  HOL_basic_ss
-    addsimps simp_thms
-    addsimps [@{thm beta_cfun}]
-    addsimprocs [@{simproc cont_proc}];
+val beta_rules =
+  @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+  @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
+
+val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
 
 fun define_consts
     (specs : (binding * term * mixfix) list)
diff -r 8f9f3d61ca8c -r a1656804fcad src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri May 21 17:16:16 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat May 22 08:30:40 2010 -0700
@@ -34,11 +34,11 @@
 structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
 struct
 
-val beta_ss =
-  HOL_basic_ss
-    addsimps simp_thms
-    addsimps [@{thm beta_cfun}]
-    addsimprocs [@{simproc cont_proc}];
+val beta_rules =
+  @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+  @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_split'};
+
+val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
 
 val beta_tac = simp_tac beta_ss;
 
diff -r 8f9f3d61ca8c -r a1656804fcad src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri May 21 17:16:16 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Sat May 22 08:30:40 2010 -0700
@@ -101,11 +101,11 @@
     take_induct_thms    : thm list
   };
 
-val beta_ss =
-  HOL_basic_ss
-    addsimps simp_thms
-    addsimps [@{thm beta_cfun}]
-    addsimprocs [@{simproc cont_proc}];
+val beta_rules =
+  @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+  @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
+
+val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
 
 val beta_tac = simp_tac beta_ss;