1.1 --- a/src/HOL/IMP/ASM.thy Fri Oct 21 08:42:11 2011 +0200
1.2 +++ b/src/HOL/IMP/ASM.thy Fri Oct 21 09:51:45 2011 +0200
1.3 @@ -4,7 +4,7 @@
1.4
1.5 subsection "Arithmetic Stack Machine"
1.6
1.7 -datatype ainstr = LOADI val | LOAD string | ADD
1.8 +datatype ainstr = LOADI val | LOAD vname | ADD
1.9
1.10 type_synonym stack = "val list"
1.11
2.1 --- a/src/HOL/Orderings.thy Fri Oct 21 08:42:11 2011 +0200
2.2 +++ b/src/HOL/Orderings.thy Fri Oct 21 09:51:45 2011 +0200
2.3 @@ -883,7 +883,7 @@
2.4 text {* These support proving chains of decreasing inequalities
2.5 a >= b >= c ... in Isar proofs. *}
2.6
2.7 -lemma xt1:
2.8 +lemma xt1 [no_atp]:
2.9 "a = b ==> b > c ==> a > c"
2.10 "a > b ==> b = c ==> a > c"
2.11 "a = b ==> b >= c ==> a >= c"
2.12 @@ -902,39 +902,39 @@
2.13 "a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c"
2.14 by auto
2.15
2.16 -lemma xt2:
2.17 +lemma xt2 [no_atp]:
2.18 "(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
2.19 by (subgoal_tac "f b >= f c", force, force)
2.20
2.21 -lemma xt3: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==>
2.22 +lemma xt3 [no_atp]: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==>
2.23 (!!x y. x >= y ==> f x >= f y) ==> f a >= c"
2.24 by (subgoal_tac "f a >= f b", force, force)
2.25
2.26 -lemma xt4: "(a::'a::order) > f b ==> (b::'b::order) >= c ==>
2.27 +lemma xt4 [no_atp]: "(a::'a::order) > f b ==> (b::'b::order) >= c ==>
2.28 (!!x y. x >= y ==> f x >= f y) ==> a > f c"
2.29 by (subgoal_tac "f b >= f c", force, force)
2.30
2.31 -lemma xt5: "(a::'a::order) > b ==> (f b::'b::order) >= c==>
2.32 +lemma xt5 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) >= c==>
2.33 (!!x y. x > y ==> f x > f y) ==> f a > c"
2.34 by (subgoal_tac "f a > f b", force, force)
2.35
2.36 -lemma xt6: "(a::'a::order) >= f b ==> b > c ==>
2.37 +lemma xt6 [no_atp]: "(a::'a::order) >= f b ==> b > c ==>
2.38 (!!x y. x > y ==> f x > f y) ==> a > f c"
2.39 by (subgoal_tac "f b > f c", force, force)
2.40
2.41 -lemma xt7: "(a::'a::order) >= b ==> (f b::'b::order) > c ==>
2.42 +lemma xt7 [no_atp]: "(a::'a::order) >= b ==> (f b::'b::order) > c ==>
2.43 (!!x y. x >= y ==> f x >= f y) ==> f a > c"
2.44 by (subgoal_tac "f a >= f b", force, force)
2.45
2.46 -lemma xt8: "(a::'a::order) > f b ==> (b::'b::order) > c ==>
2.47 +lemma xt8 [no_atp]: "(a::'a::order) > f b ==> (b::'b::order) > c ==>
2.48 (!!x y. x > y ==> f x > f y) ==> a > f c"
2.49 by (subgoal_tac "f b > f c", force, force)
2.50
2.51 -lemma xt9: "(a::'a::order) > b ==> (f b::'b::order) > c ==>
2.52 +lemma xt9 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) > c ==>
2.53 (!!x y. x > y ==> f x > f y) ==> f a > c"
2.54 by (subgoal_tac "f a > f b", force, force)
2.55
2.56 -lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9
2.57 +lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 [no_atp]
2.58
2.59 (*
2.60 Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands