# HG changeset patch # User berghofe # Date 1188316996 -7200 # Node ID 93b113c5ac332e41e60fd47cacf6f64e085763ef # Parent 7c205d006719119701f1ed9acd3cfbbe1452c9ec - theorem(_i) now also takes "interactive" flag as argument - added theorem hook diff -r 7c205d006719 -r 93b113c5ac33 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Tue Aug 28 18:01:37 2007 +0200 +++ b/src/Pure/Isar/specification.ML Tue Aug 28 18:03:16 2007 +0200 @@ -42,10 +42,11 @@ -> local_theory -> (bstring * thm list) list * local_theory val theorem: string -> Method.text option -> (thm list list -> local_theory -> local_theory) -> string * Attrib.src list -> Element.context Locale.element list -> Element.statement -> - local_theory -> Proof.state + bool -> local_theory -> Proof.state val theorem_i: string -> Method.text option -> (thm list list -> local_theory -> local_theory) -> string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i -> - local_theory -> Proof.state + bool -> local_theory -> Proof.state + val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic end; structure Specification: SPECIFICATION = @@ -244,8 +245,16 @@ [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths); in ((prems, stmt, facts), goal_ctxt) end); +structure TheoremHook = GenericDataFun +( + type T = ((bool -> Proof.state -> Proof.state) * stamp) list; + val empty = []; + val extend = I; + fun merge _ type_checks : T = Library.merge (eq_snd op =) type_checks; +); + fun gen_theorem prep_att prep_stmt - kind before_qed after_qed (name, raw_atts) raw_elems raw_concl lthy0 = + kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy0 = let val _ = LocalTheory.affirm lthy0; val thy = ProofContext.theory_of lthy0; @@ -280,6 +289,8 @@ |> ProofContext.note_thmss_i Thm.assumptionK [((AutoBind.assmsN, []), [(prems, [])])] |> snd |> Proof.theorem_i before_qed after_qed' (map snd stmt) + |> Library.apply (map (fn (f, _) => f int) + (TheoremHook.get (Context.Proof goal_ctxt))) |> Proof.refine_insert facts end; @@ -288,6 +299,8 @@ val theorem = gen_theorem Attrib.intern_src Locale.read_context_statement_i; val theorem_i = gen_theorem (K I) Locale.cert_context_statement; +fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ())); + end; end;