get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
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