# HG changeset patch # User berghofe # Date 1160756118 -7200 # Node ID 9af9ceb16d584c06e47aaae498c97c3da3c0d40c # Parent 650c48711c7b69d948e5affe27a768fc18ed5d8d Adapted to changes in FixedPoint theory. diff -r 650c48711c7b -r 9af9ceb16d58 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Fri Oct 13 18:14:12 2006 +0200 +++ b/src/HOL/Hilbert_Choice.thy Fri Oct 13 18:15:18 2006 +0200 @@ -419,7 +419,7 @@ lemma GreatestM_nat_le: "P x ==> \y. P y --> m y < b ==> (m x::nat) <= m (GreatestM m P)" - apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec]) + apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec, of P]) done diff -r 650c48711c7b -r 9af9ceb16d58 src/HOL/Hyperreal/Transcendental.thy --- a/src/HOL/Hyperreal/Transcendental.thy Fri Oct 13 18:14:12 2006 +0200 +++ b/src/HOL/Hyperreal/Transcendental.thy Fri Oct 13 18:15:18 2006 +0200 @@ -1942,7 +1942,7 @@ lemma real_root_eq_iff [simp]: "[| 0 \ x; 0 \ y |] ==> (root(Suc n) x = root(Suc n) y) = (x = y)" -apply (auto intro!: order_antisym) +apply (auto intro!: order_antisym [where 'a = real]) apply (rule_tac n1 = n in real_root_le_iff [THEN iffD1]) apply (rule_tac [4] n1 = n in real_root_le_iff [THEN iffD1], auto) done diff -r 650c48711c7b -r 9af9ceb16d58 src/HOL/IMP/Denotation.thy --- a/src/HOL/IMP/Denotation.thy Fri Oct 13 18:14:12 2006 +0200 +++ b/src/HOL/IMP/Denotation.thy Fri Oct 13 18:15:18 2006 +0200 @@ -62,7 +62,7 @@ apply fast (* while *) -apply (erule lfp_induct [OF _ Gamma_mono]) +apply (erule lfp_induct_set [OF _ Gamma_mono]) apply (unfold Gamma_def) apply fast done diff -r 650c48711c7b -r 9af9ceb16d58 src/HOL/NanoJava/Example.thy --- a/src/HOL/NanoJava/Example.thy Fri Oct 13 18:14:12 2006 +0200 +++ b/src/HOL/NanoJava/Example.thy Fri Oct 13 18:15:18 2006 +0200 @@ -92,17 +92,17 @@ "s:x\Suc n = (\a. x=Addr a \ heap s a \ None \ s:get_field s a pred\n)" lemma Nat_atleast_lupd [rule_format, simp]: - "\s v. lupd(x\y) s:v \ n = (s:v \ n)" + "\s v::val. lupd(x\y) s:v \ n = (s:v \ n)" apply (induct n) by auto lemma Nat_atleast_set_locs [rule_format, simp]: - "\s v. set_locs l s:v \ n = (s:v \ n)" + "\s v::val. set_locs l s:v \ n = (s:v \ n)" apply (induct n) by auto lemma Nat_atleast_del_locs [rule_format, simp]: - "\s v. del_locs s:v \ n = (s:v \ n)" + "\s v::val. del_locs s:v \ n = (s:v \ n)" apply (induct n) by auto @@ -121,7 +121,7 @@ by auto lemma Nat_atleast_newC [rule_format]: - "heap s aa = None \ \v. s:v \ n \ hupd(aa\obj) s:v \ n" + "heap s aa = None \ \v::val. s:v \ n \ hupd(aa\obj) s:v \ n" apply (induct n) apply auto apply (case_tac "aa=a") diff -r 650c48711c7b -r 9af9ceb16d58 src/HOL/TLA/Intensional.thy --- a/src/HOL/TLA/Intensional.thy Fri Oct 13 18:14:12 2006 +0200 +++ b/src/HOL/TLA/Intensional.thy Fri Oct 13 18:15:18 2006 +0200 @@ -180,7 +180,7 @@ Valid_def: "|- A == ALL w. w |= A" unl_con: "LIFT #c w == c" - unl_lift: "LIFT f w == f (x w)" + unl_lift: "lift f x w == f (x w)" unl_lift2: "LIFT f w == f (x w) (y w)" unl_lift3: "LIFT f w == f (x w) (y w) (z w)"