src/HOL/Tools/SMT2/z3_new_replay_util.ML

   val compose: compose_data -> thm -> thm
 
   (*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 =
   let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm)

     net
 
 end
 
 
-
 (* proof combinators *)
 
 fun under_assumption f ct =
   let val ct' = SMT2_Util.mk_cprop ct in Thm.implies_intr ct' (f (Thm.assume ct')) end
 
 fun discharge p pq = Thm.implies_elim pq p
-
 
 
 (* a faster COMP *)
 
 type compose_data = cterm list * (cterm -> cterm list) * thm

 fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
 fun precompose2 f rule = precompose (list2 o f) rule
 
 fun compose (cvs, f, rule) thm =
   discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
-
 
 
 (* simpset *)
 
 local

 fun make_simpset ctxt rules =
   simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt addsimps rules)
 
 end
 
-end
+end;