src/Pure/Isar/skip_proof.ML
changeset 26530 777f334ff652
parent 26463 9283b4185fdf
child 26711 3a478bfa1650
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Thu Apr 03 16:34:52 2008 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Thu Apr 03 17:43:01 2008 +0200
     1.3 @@ -11,6 +11,8 @@
     1.4    val cheat_tac: theory -> tactic
     1.5    val prove: Proof.context -> string list -> term list -> term ->
     1.6      ({prems: thm list, context: Proof.context} -> tactic) -> thm
     1.7 +  val prove_global: theory -> string list -> term list -> term ->
     1.8 +    (thm list -> tactic) -> thm
     1.9  end;
    1.10  
    1.11  structure SkipProof: SKIP_PROOF =
    1.12 @@ -42,4 +44,7 @@
    1.13      then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
    1.14      else tac args st);
    1.15  
    1.16 +fun prove_global thy xs asms prop tac =
    1.17 +  Drule.standard (prove (ProofContext.init thy) xs asms prop (fn {prems, ...} => tac prems));
    1.18 +
    1.19  end;