# HG changeset patch
# User wenzelm
# Date 938701016 -7200
# Node ID 8c3190b173aa8408dbd17d7948b30c701a87db41
# Parent  7e38237edfcb65cdfa437d394945aee08b1699d6
depend on Main;

diff -r 7e38237edfcb -r 8c3190b173aa src/HOLCF/Cprod1.ML
--- a/src/HOLCF/Cprod1.ML	Thu Sep 30 10:06:56 1999 +0200
+++ b/src/HOLCF/Cprod1.ML	Thu Sep 30 16:16:56 1999 +0200
@@ -13,7 +13,7 @@
 (* less_cprod is a partial order on 'a * 'b                                 *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "Sel_injective_cprod" Prod.thy 
+qed_goal "Sel_injective_cprod" Prod.thy
         "[|fst x = fst y; snd x = snd y|] ==> x = y"
 (fn prems =>
         [
@@ -21,7 +21,7 @@
         (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1),
         (rotate_tac ~1 1),
         (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1),
-        (Asm_simp_tac 1)
+        (asm_simp_tac (simpset_of Prod.thy) 1)
         ]);
 
 qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "(p::'a*'b) << p"
diff -r 7e38237edfcb -r 8c3190b173aa src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Thu Sep 30 10:06:56 1999 +0200
+++ b/src/HOLCF/Fix.ML	Thu Sep 30 16:16:56 1999 +0200
@@ -692,7 +692,7 @@
   val adm_disj_lemma4 = prove_goal Arith.thy
   "!!Q. !j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
  (fn _ =>
-        [Asm_simp_tac 1]);
+        [asm_simp_tac (simpset_of Arith.thy) 1]);
 
   val adm_disj_lemma5 = prove_goal thy
   "!!Y::nat=>'a::cpo. [| chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
@@ -881,7 +881,7 @@
         etac adm_disj 1,
         atac 1]);
 
-val adm_lemmas = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
-        adm_all2,adm_not_less,adm_not_conj,adm_iff];
+bind_thms ("adm_lemmas", [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
+        adm_all2,adm_not_less,adm_not_conj,adm_iff]);
 
 Addsimps adm_lemmas;
diff -r 7e38237edfcb -r 8c3190b173aa src/HOLCF/IOA/meta_theory/Asig.thy
--- a/src/HOLCF/IOA/meta_theory/Asig.thy	Thu Sep 30 10:06:56 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/Asig.thy	Thu Sep 30 16:16:56 1999 +0200
@@ -6,7 +6,7 @@
 Action signatures
 *)
 
-Asig = Arith +
+Asig = Main +
 
 types 
 
diff -r 7e38237edfcb -r 8c3190b173aa src/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Sep 30 10:06:56 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Sep 30 16:16:56 1999 +0200
@@ -214,7 +214,7 @@
 (* ------------------------- renaming ------------------------------------------- *)
   
 rename_set_def
-  "rename_set set ren == {b. ? x. Some x = ren b & x : set}" 
+  "rename_set A ren == {b. ? x. Some x = ren b & x : A}" 
 
 rename_def 
 "rename ioa ren ==  
diff -r 7e38237edfcb -r 8c3190b173aa src/HOLCF/IOA/meta_theory/Pred.thy
--- a/src/HOLCF/IOA/meta_theory/Pred.thy	Thu Sep 30 10:06:56 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Thu Sep 30 16:16:56 1999 +0200
@@ -7,7 +7,7 @@
 
 *)   
 	       
-Pred = Arith +  
+Pred = Main +
 
 default term
 
@@ -68,4 +68,4 @@
 IMPLIES_def
   "(P .--> Q) s == (P s) --> (Q s)"
 
-end
\ No newline at end of file
+end
diff -r 7e38237edfcb -r 8c3190b173aa src/HOLCF/Porder0.thy
--- a/src/HOLCF/Porder0.thy	Thu Sep 30 10:06:56 1999 +0200
+++ b/src/HOLCF/Porder0.thy	Thu Sep 30 16:16:56 1999 +0200
@@ -7,7 +7,7 @@
 
 *)
 
-Porder0 = Arith +
+Porder0 = Main +
 
 	(* introduce a (syntactic) class for the constant << *)
 axclass sq_ord<term