# HG changeset patch
# User wenzelm
# Date 1273940958 -7200
# Node ID 524a3172db5ba89738b0c4826fb197ce925d15f4
# Parent  fdefcbcb28878a9b21a7db07a7b5c8889359f1e4# Parent  897ee863885dc88f6d6ad3133493ef4cb79d7a05
merged

diff -r 897ee863885d -r 524a3172db5b src/HOL/RealDef.thy
--- 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]
diff -r 897ee863885d -r 524a3172db5b src/HOL/Tools/SMT/smt_solver.ML
--- 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)
diff -r 897ee863885d -r 524a3172db5b src/HOL/Tools/SMT/z3_proof_parser.ML
--- 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