--- a/src/HOL/Tools/SMT2/z3_new_replay_util.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_util.ML Thu Jun 12 01:00:49 2014 +0200
@@ -23,13 +23,11 @@
(*simpset*)
val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
val make_simpset: Proof.context -> thm list -> simpset
-end
+end;
structure Z3_New_Replay_Util: Z3_NEW_REPLAY_UTIL =
struct
-
-
(* theorem nets *)
fun thm_net_of f xthms =
@@ -59,7 +57,6 @@
end
-
(* proof combinators *)
fun under_assumption f ct =
@@ -68,7 +65,6 @@
fun discharge p pq = Thm.implies_elim pq p
-
(* a faster COMP *)
type compose_data = cterm list * (cterm -> cterm list) * thm
@@ -82,7 +78,6 @@
discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
-
(* simpset *)
local
@@ -152,4 +147,4 @@
end
-end
+end;