Prove.thy
author Christian Urban <urbanc@in.tum.de>
Mon, 28 Sep 2009 23:17:29 +0200
changeset 48 5d32a81cfe49
parent 46 e801b929216b
child 57 13be92f5b638
permissions -rw-r--r--
added name to prove

theory Prove
imports Main
begin

ML {*
val r = ref (NONE:(unit -> term) option)
*}

ML {*
let
  fun after_qed thm_name thms lthy =
       LocalTheory.note Thm.theoremK (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