Adapted to changes in FixedPoint theory.
authorberghofe
Fri Oct 13 18:15:18 2006 +0200 (2006-10-13)
changeset 210209af9ceb16d58
parent 21019 650c48711c7b
child 21021 6f19e5eb3a44
Adapted to changes in FixedPoint theory.
src/HOL/Hilbert_Choice.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/IMP/Denotation.thy
src/HOL/NanoJava/Example.thy
src/HOL/TLA/Intensional.thy
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Oct 13 18:14:12 2006 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Oct 13 18:15:18 2006 +0200
     1.3 @@ -419,7 +419,7 @@
     1.4  lemma GreatestM_nat_le:
     1.5    "P x ==> \<forall>y. P y --> m y < b
     1.6      ==> (m x::nat) <= m (GreatestM m P)"
     1.7 -  apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec])
     1.8 +  apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec, of P])
     1.9    done
    1.10  
    1.11  
     2.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Fri Oct 13 18:14:12 2006 +0200
     2.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Fri Oct 13 18:15:18 2006 +0200
     2.3 @@ -1942,7 +1942,7 @@
     2.4  
     2.5  lemma real_root_eq_iff [simp]:
     2.6       "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x = root(Suc n) y) = (x = y)"
     2.7 -apply (auto intro!: order_antisym)
     2.8 +apply (auto intro!: order_antisym [where 'a = real])
     2.9  apply (rule_tac n1 = n in real_root_le_iff [THEN iffD1])
    2.10  apply (rule_tac [4] n1 = n in real_root_le_iff [THEN iffD1], auto)
    2.11  done
     3.1 --- a/src/HOL/IMP/Denotation.thy	Fri Oct 13 18:14:12 2006 +0200
     3.2 +++ b/src/HOL/IMP/Denotation.thy	Fri Oct 13 18:15:18 2006 +0200
     3.3 @@ -62,7 +62,7 @@
     3.4  apply fast
     3.5  
     3.6  (* while *)
     3.7 -apply (erule lfp_induct [OF _ Gamma_mono])
     3.8 +apply (erule lfp_induct_set [OF _ Gamma_mono])
     3.9  apply (unfold Gamma_def)
    3.10  apply fast
    3.11  done
     4.1 --- a/src/HOL/NanoJava/Example.thy	Fri Oct 13 18:14:12 2006 +0200
     4.2 +++ b/src/HOL/NanoJava/Example.thy	Fri Oct 13 18:15:18 2006 +0200
     4.3 @@ -92,17 +92,17 @@
     4.4          "s:x\<ge>Suc n = (\<exists>a. x=Addr a \<and> heap s a \<noteq> None \<and> s:get_field s a pred\<ge>n)"
     4.5  
     4.6  lemma Nat_atleast_lupd [rule_format, simp]: 
     4.7 - "\<forall>s v. lupd(x\<mapsto>y) s:v \<ge> n = (s:v \<ge> n)"
     4.8 + "\<forall>s v::val. lupd(x\<mapsto>y) s:v \<ge> n = (s:v \<ge> n)"
     4.9  apply (induct n)
    4.10  by  auto
    4.11  
    4.12  lemma Nat_atleast_set_locs [rule_format, simp]: 
    4.13 - "\<forall>s v. set_locs l s:v \<ge> n = (s:v \<ge> n)"
    4.14 + "\<forall>s v::val. set_locs l s:v \<ge> n = (s:v \<ge> n)"
    4.15  apply (induct n)
    4.16  by auto
    4.17  
    4.18  lemma Nat_atleast_del_locs [rule_format, simp]: 
    4.19 - "\<forall>s v. del_locs s:v \<ge> n = (s:v \<ge> n)"
    4.20 + "\<forall>s v::val. del_locs s:v \<ge> n = (s:v \<ge> n)"
    4.21  apply (induct n)
    4.22  by auto
    4.23  
    4.24 @@ -121,7 +121,7 @@
    4.25  by auto
    4.26  
    4.27  lemma Nat_atleast_newC [rule_format]: 
    4.28 -  "heap s aa = None \<Longrightarrow> \<forall>v. s:v \<ge> n \<longrightarrow> hupd(aa\<mapsto>obj) s:v \<ge> n"
    4.29 +  "heap s aa = None \<Longrightarrow> \<forall>v::val. s:v \<ge> n \<longrightarrow> hupd(aa\<mapsto>obj) s:v \<ge> n"
    4.30  apply (induct n)
    4.31  apply  auto
    4.32  apply  (case_tac "aa=a")
     5.1 --- a/src/HOL/TLA/Intensional.thy	Fri Oct 13 18:14:12 2006 +0200
     5.2 +++ b/src/HOL/TLA/Intensional.thy	Fri Oct 13 18:15:18 2006 +0200
     5.3 @@ -180,7 +180,7 @@
     5.4    Valid_def:   "|- A    ==  ALL w. w |= A"
     5.5  
     5.6    unl_con:     "LIFT #c w  ==  c"
     5.7 -  unl_lift:    "LIFT f<x> w == f (x w)"
     5.8 +  unl_lift:    "lift f x w == f (x w)"
     5.9    unl_lift2:   "LIFT f<x, y> w == f (x w) (y w)"
    5.10    unl_lift3:   "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
    5.11