1 theory Prove

     2 imports Main

     3 begin

     4 

     5 ML {*

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

     7 *}

     8 ML {*

     9 let

    10    fun setup_proof (txt, pos) lthy =

    11    let

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

    13    in

    14        Proof.theorem_i NONE (K I) [[(trm,[])]] lthy

    15    end;

    16 

    17    val setup_proof_parser = OuterParse.ML_source >> setup_proof

    18         

    19    val kind = OuterKeyword.thy_goal

    20 in

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

    22     kind setup_proof_parser

    23 end

    24 *}

    25 

    26 end