1 theory Prove

     2 imports Plain 

     3 begin

     4 

     5 ML {*

     6 val r = Unsynchronized.ref (NONE:(unit -> term) option)

     7 *}

     8 

     9 ML {*

    10 let

    11   fun after_qed thm_name thms lthy =

    12     Local_Theory.note (thm_name, (flat thms)) lthy |> snd

    13   fun setup_proof (name_spec, (txt, _)) lthy =

    14   let

    15     val trm = ML_Context.evaluate lthy true ("r", r) txt

    16   in

    17     Proof.theorem NONE (after_qed name_spec) [[(trm,[])]] lthy

    18   end

    19 

    20   val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source

    21 in

    22   Outer_Syntax.local_theory_to_proof "prove" "proving a proposition" 

    23     Keyword.thy_goal (parser >> setup_proof)

    24 end

    25 *}

    26 

    27 end