src/Pure/Isar/skip_proof.ML
changeset 32970 fbd2bb2489a8
parent 32966 5b21661fe618
child 35021 c839a4c670c6
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Sat Oct 17 16:40:41 2009 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Sat Oct 17 16:58:03 2009 +0200
     1.3 @@ -1,7 +1,8 @@
     1.4  (*  Title:      Pure/Isar/skip_proof.ML
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Skipping proofs -- quick_and_dirty mode.
     1.8 +Skipping proofs -- via oracle (in quick and dirty mode) or by forking
     1.9 +(parallel mode).
    1.10  *)
    1.11  
    1.12  signature SKIP_PROOF =
    1.13 @@ -14,15 +15,13 @@
    1.14      ({prems: thm list, context: Proof.context} -> tactic) -> thm
    1.15  end;
    1.16  
    1.17 -structure SkipProof: SKIP_PROOF =
    1.18 +structure Skip_Proof: SKIP_PROOF =
    1.19  struct
    1.20  
    1.21  (* oracle setup *)
    1.22  
    1.23  val (_, skip_proof) = Context.>>> (Context.map_theory_result
    1.24 -  (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) =>
    1.25 -    if ! quick_and_dirty then Thm.cterm_of thy prop
    1.26 -    else error "Proof may be skipped in quick_and_dirty mode only!")));
    1.27 +  (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) => Thm.cterm_of thy prop)));
    1.28  
    1.29  
    1.30  (* basic cheating *)
    1.31 @@ -36,7 +35,7 @@
    1.32    (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
    1.33      (fn args => fn st =>
    1.34        if ! quick_and_dirty
    1.35 -      then setmp_CRITICAL quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
    1.36 +      then cheat_tac (ProofContext.theory_of ctxt) st
    1.37        else tac args st);
    1.38  
    1.39  fun prove_global thy xs asms prop tac =