# 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