--- a/src/HOL/SPARK/SPARK.thy Thu Jan 10 21:20:14 2013 +0100
+++ b/src/HOL/SPARK/SPARK.thy Thu Jan 10 23:02:58 2013 +0100
@@ -275,4 +275,11 @@
qed
qed
+
+text {* Minimum and maximum *}
+
+spark_proof_functions
+ integer__min = "min :: int \<Rightarrow> int \<Rightarrow> int"
+ integer__max = "max :: int \<Rightarrow> int \<Rightarrow> int"
+
end
--- a/src/HOL/SPARK/Tools/spark_commands.ML Thu Jan 10 21:20:14 2013 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Thu Jan 10 23:02:58 2013 +0100
@@ -75,7 +75,7 @@
Specification.theorem Thm.theoremK NONE
(fn thmss => (Local_Theory.background_theory
(SPARK_VCs.mark_proved vc_name (flat thmss))))
- (Binding.name vc_name, []) [] ctxt stmt true lthy
+ (Binding.name vc_name, []) [] ctxt stmt false lthy
end;
fun string_of_status NONE = "(unproved)"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Thu Jan 10 21:20:14 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Thu Jan 10 23:02:58 2013 +0100
@@ -69,7 +69,8 @@
in
fun handle_metis_fail try_metis () =
try_metis () handle exp =>
- (if debug then raise exp else metis_fail := true; SOME Time.zeroTime)
+ (if Exn.is_interrupt exp orelse debug then reraise exp
+ else metis_fail := true; SOME Time.zeroTime)
fun get_time lazy_time =
if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time
val metis_fail = fn () => !metis_fail
@@ -125,7 +126,7 @@
|> maps (thms_of_name ctxt)
(* TODO: add "Obtain" case *)
- exception ZeroTime
+ exception ZEROTIME
fun try_metis timeout (succedent, step) =
(if not preplay then K (SOME Time.zeroTime) else
let
@@ -157,7 +158,7 @@
in
(prop, byline, true)
end
- | _ => raise ZeroTime)
+ | _ => raise ZEROTIME)
val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
val facts =
(case byline of
@@ -182,7 +183,7 @@
in
take_time timeout (fn () => goal tac)
end)
- handle ZeroTime => K (SOME Time.zeroTime)
+ handle ZEROTIME => K (SOME Time.zeroTime)
val try_metis_quietly = the_default NONE oo try oo try_metis
@@ -208,11 +209,12 @@
(Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) =>
(fn by => Prove (qs2, label2, t, by), lfs2, gfs2)
| (Obtain(qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
- (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2) )
+ (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2)
+ | _ => error "Internal error: unmergeable Isar steps" )
val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
val gfs = union (op =) gfs1 gfs2
in step_constructor (By_Metis (lfs, gfs)) end
- | merge _ _ = error "Internal error: Unmergeable Isar steps"
+ | merge _ _ = error "Internal error: unmergeable Isar steps"
fun try_merge metis_time (s1, i) (s2, j) =
(case get i metis_time |> Lazy.force of