--- a/src/HOL/RealDef.thy Sat May 15 18:15:50 2010 +0200
+++ b/src/HOL/RealDef.thy Sat May 15 18:29:18 2010 +0200
@@ -1055,6 +1055,7 @@
lemmas real_le_refl = order_refl [of "w::real", standard]
lemmas real_le_antisym = order_antisym [of "z::real" "w", standard]
lemmas real_le_trans = order_trans [of "i::real" "j" "k", standard]
+lemmas real_le_linear = linear [of "z::real" "w", standard]
lemmas real_le_eq_diff = le_iff_diff_le_0 [of "x::real" "y", standard]
lemmas real_add_left_mono = add_left_mono [of "x::real" "y" "z", standard]
lemmas real_mult_order = mult_pos_pos [of "x::real" "y", standard]
--- a/src/HOL/Tools/SMT/smt_solver.ML Sat May 15 18:15:50 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Sat May 15 18:29:18 2010 +0200
@@ -166,7 +166,7 @@
end
-fun trace_recon_data ctxt {typs, terms, ...} =
+fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
let
fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
fun pretty_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Sat May 15 18:15:50 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Sat May 15 18:29:18 2010 +0200
@@ -285,15 +285,15 @@
"4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
"8" => SOME 8 | "9" => SOME 9 | _ => NONE)
-val digits = Scan.lift (Scan.many1 Symbol.is_ascii_digit) >> implode
-val nat_num = Scan.lift (Scan.repeat1 (Scan.some digit)) >> (fn ds =>
- fold (fn d => fn i => i * 10 + d) ds 0)
-val int_num = Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
- (fn sign => nat_num >> sign)
+fun digits st = (Scan.lift (Scan.many1 Symbol.is_ascii_digit) >> implode) st
+fun nat_num st = (Scan.lift (Scan.repeat1 (Scan.some digit)) >> (fn ds =>
+ fold (fn d => fn i => i * 10 + d) ds 0)) st
+fun int_num st = (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
+ (fn sign => nat_num >> sign)) st
val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
-val name = Scan.lift (Scan.many1 is_char) >> implode
+fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st
fun sym st =
(name -- Scan.optional (bra (seps_by ($$ ":") sym)) [] >> I.Sym) st