1(*---------------------------------------------------------------------------*) 2(* This structure is used by Holmake to provide a "fast" mode of running *) 3(* theory scripts. It toggles the prover that sits behind the prove *) 4(* (and store_thm) function to be a call to mk_thm, so proofs that require *) 5(* many cycles should now run very quickly. Of course, the tactic value *) 6(* still has to be evaluated before it is then discarded. But use of this *) 7(* can definitely speed slow scripts up considerably. *) 8(*---------------------------------------------------------------------------*) 9 10structure fastbuild = 11struct 12 13local 14 open Feedback Thm 15 16 val fast_proof_tag = "fast_proof" 17 18 fun fast_prover (t, tac: Abbrev.tactic) = 19 mk_oracle_thm fast_proof_tag ([], t) 20 21 fun first_fast_prover (t, tac: Abbrev.tactic) = 22 (HOL_MESG "using fast prover - proofs unchecked" 23 ; Tactical.set_prover fast_prover 24 ; mk_oracle_thm fast_proof_tag ([], t)) 25in 26 val () = Tactical.set_prover first_fast_prover 27end 28 29end 30