src/Pure/Isar/skip_proof.ML
changeset 11732 139aaced13f4
parent 8807 0046be1769f9
child 11892 4a8834757140
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Fri Oct 12 12:09:21 2001 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Fri Oct 12 12:09:38 2001 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4      -> Proof.state -> Proof.state Seq.seq
     1.5    val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
     1.6    val prove_goalw_cterm: theory -> thm list -> cterm -> (thm list -> tactic list) -> thm
     1.7 +  val make_thm: theory -> term -> thm
     1.8    val setup: (theory -> theory) list
     1.9  end;
    1.10  
    1.11 @@ -58,6 +59,12 @@
    1.12      (if ! quick_and_dirty then (K [cheat_tac thy]) else tacs);
    1.13  
    1.14  
    1.15 +(* make_thm *)
    1.16 +
    1.17 +fun make_thm thy t =
    1.18 +  prove_goalw_cterm thy [] (Thm.cterm_of (Theory.sign_of thy) t) (K []);
    1.19 +
    1.20 +
    1.21  (* theory setup *)
    1.22  
    1.23  val setup = [Theory.add_oracle (skip_proofN, any_thm)];