--- 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"
--- 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;
--- 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
--- 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 ==
--- 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
--- 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