depend on Main;
authorwenzelm
Thu Sep 30 16:16:56 1999 +0200 (1999-09-30)
changeset 76618c3190b173aa
parent 7660 7e38237edfcb
child 7662 062a782d7402
depend on Main;
src/HOLCF/Cprod1.ML
src/HOLCF/Fix.ML
src/HOLCF/IOA/meta_theory/Asig.thy
src/HOLCF/IOA/meta_theory/Automata.thy
src/HOLCF/IOA/meta_theory/Pred.thy
src/HOLCF/Porder0.thy
     1.1 --- a/src/HOLCF/Cprod1.ML	Thu Sep 30 10:06:56 1999 +0200
     1.2 +++ b/src/HOLCF/Cprod1.ML	Thu Sep 30 16:16:56 1999 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  (* less_cprod is a partial order on 'a * 'b                                 *)
     1.5  (* ------------------------------------------------------------------------ *)
     1.6  
     1.7 -qed_goal "Sel_injective_cprod" Prod.thy 
     1.8 +qed_goal "Sel_injective_cprod" Prod.thy
     1.9          "[|fst x = fst y; snd x = snd y|] ==> x = y"
    1.10  (fn prems =>
    1.11          [
    1.12 @@ -21,7 +21,7 @@
    1.13          (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1),
    1.14          (rotate_tac ~1 1),
    1.15          (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1),
    1.16 -        (Asm_simp_tac 1)
    1.17 +        (asm_simp_tac (simpset_of Prod.thy) 1)
    1.18          ]);
    1.19  
    1.20  qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "(p::'a*'b) << p"
     2.1 --- a/src/HOLCF/Fix.ML	Thu Sep 30 10:06:56 1999 +0200
     2.2 +++ b/src/HOLCF/Fix.ML	Thu Sep 30 16:16:56 1999 +0200
     2.3 @@ -692,7 +692,7 @@
     2.4    val adm_disj_lemma4 = prove_goal Arith.thy
     2.5    "!!Q. !j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
     2.6   (fn _ =>
     2.7 -        [Asm_simp_tac 1]);
     2.8 +        [asm_simp_tac (simpset_of Arith.thy) 1]);
     2.9  
    2.10    val adm_disj_lemma5 = prove_goal thy
    2.11    "!!Y::nat=>'a::cpo. [| chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
    2.12 @@ -881,7 +881,7 @@
    2.13          etac adm_disj 1,
    2.14          atac 1]);
    2.15  
    2.16 -val adm_lemmas = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
    2.17 -        adm_all2,adm_not_less,adm_not_conj,adm_iff];
    2.18 +bind_thms ("adm_lemmas", [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
    2.19 +        adm_all2,adm_not_less,adm_not_conj,adm_iff]);
    2.20  
    2.21  Addsimps adm_lemmas;
     3.1 --- a/src/HOLCF/IOA/meta_theory/Asig.thy	Thu Sep 30 10:06:56 1999 +0200
     3.2 +++ b/src/HOLCF/IOA/meta_theory/Asig.thy	Thu Sep 30 16:16:56 1999 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  Action signatures
     3.5  *)
     3.6  
     3.7 -Asig = Arith +
     3.8 +Asig = Main +
     3.9  
    3.10  types 
    3.11  
     4.1 --- a/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Sep 30 10:06:56 1999 +0200
     4.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Sep 30 16:16:56 1999 +0200
     4.3 @@ -214,7 +214,7 @@
     4.4  (* ------------------------- renaming ------------------------------------------- *)
     4.5    
     4.6  rename_set_def
     4.7 -  "rename_set set ren == {b. ? x. Some x = ren b & x : set}" 
     4.8 +  "rename_set A ren == {b. ? x. Some x = ren b & x : A}" 
     4.9  
    4.10  rename_def 
    4.11  "rename ioa ren ==  
     5.1 --- a/src/HOLCF/IOA/meta_theory/Pred.thy	Thu Sep 30 10:06:56 1999 +0200
     5.2 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Thu Sep 30 16:16:56 1999 +0200
     5.3 @@ -7,7 +7,7 @@
     5.4  
     5.5  *)   
     5.6  	       
     5.7 -Pred = Arith +  
     5.8 +Pred = Main +
     5.9  
    5.10  default term
    5.11  
    5.12 @@ -68,4 +68,4 @@
    5.13  IMPLIES_def
    5.14    "(P .--> Q) s == (P s) --> (Q s)"
    5.15  
    5.16 -end
    5.17 \ No newline at end of file
    5.18 +end
     6.1 --- a/src/HOLCF/Porder0.thy	Thu Sep 30 10:06:56 1999 +0200
     6.2 +++ b/src/HOLCF/Porder0.thy	Thu Sep 30 16:16:56 1999 +0200
     6.3 @@ -7,7 +7,7 @@
     6.4  
     6.5  *)
     6.6  
     6.7 -Porder0 = Arith +
     6.8 +Porder0 = Main +
     6.9  
    6.10  	(* introduce a (syntactic) class for the constant << *)
    6.11  axclass sq_ord<term