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     

    14   fun setup_proof (name_spec, (txt, pos)) lthy =

    15   let

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

    17   in

    18     Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy

    19   end

    20 

    21   val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source

    22 in

    23   OuterSyntax.local_theory_to_proof "prove" "proving a proposition" 

    24     OuterKeyword.thy_goal (parser >> setup_proof)

    25 end

    26 *}

    27 

    28 end