theory Prove+
−
imports Plain +
−
begin+
−
+
−
ML {*+
−
val r = Unsynchronized.ref (NONE:(unit -> term) option)+
−
*}+
−
+
−
ML {*+
−
let+
−
  fun after_qed thm_name thms lthy =+
−
       Local_Theory.note (thm_name, (flat thms)) lthy |> snd+
−
    +
−
  fun setup_proof (name_spec, (txt, pos)) lthy =+
−
  let+
−
    val trm = ML_Context.evaluate lthy true ("r", r) txt+
−
  in+
−
    Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy+
−
  end+
−
+
−
  val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source+
−
in+
−
  OuterSyntax.local_theory_to_proof "prove" "proving a proposition" +
−
    OuterKeyword.thy_goal (parser >> setup_proof)+
−
end+
−
*}+
−
+
−
end+
−