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