Changed to the use of "modern interface"
(removed the _cmd and passing of strings)
Fixed Trueprop handling and the first proof starts working properly.
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+ −