src/Pure/Isar/skip_proof.ML
changeset 11972 15da572c3c27
parent 11892 4a8834757140
child 12055 a9c44895cc8c
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Sat Oct 27 23:19:37 2001 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Sat Oct 27 23:19:55 2001 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    val quick_and_dirty: bool ref
     1.5    val make_thm: theory -> term -> thm
     1.6    val cheat_tac: theory -> tactic
     1.7 +  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
     1.8    val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
     1.9      -> Proof.state -> Proof.state Seq.seq
    1.10    val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    1.11 @@ -40,7 +41,7 @@
    1.12  val setup = [Theory.add_oracle (skip_proofN, skip_proof)];
    1.13  
    1.14  
    1.15 -(* make_thm and cheat_tac *)
    1.16 +(* basic cheating *)
    1.17  
    1.18  fun make_thm thy t =
    1.19    (*dynamic scoping of the oracle, cannot even qualify the name due to Pure/CPure!*)
    1.20 @@ -49,6 +50,10 @@
    1.21  fun cheat_tac thy st =
    1.22    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
    1.23  
    1.24 +fun prove thy xs asms prop tac =
    1.25 +  Tactic.prove (Theory.sign_of thy) xs asms prop
    1.26 +    (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
    1.27 +
    1.28  
    1.29  (* "sorry" proof command *)
    1.30