theory Prove

imports Main

begin

ML {*

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

*}

ML {*

let

   fun setup_proof (txt, pos) lthy =

   let

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

   in

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

   end;

   val setup_proof_parser = OuterParse.ML_source >> setup_proof

   val kind = OuterKeyword.thy_goal

in

  OuterSyntax.local_theory_to_proof "prove" "proving a proposition" 

    kind setup_proof_parser

end

*}

end