src/Pure/Isar/specification.ML
changeset 24452 93b113c5ac33
parent 24219 e558fe311376
child 24464 58d24cbe5fa6
     1.1 --- a/src/Pure/Isar/specification.ML	Tue Aug 28 18:01:37 2007 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Tue Aug 28 18:03:16 2007 +0200
     1.3 @@ -42,10 +42,11 @@
     1.4      -> local_theory -> (bstring * thm list) list * local_theory
     1.5    val theorem: string -> Method.text option -> (thm list list -> local_theory -> local_theory) ->
     1.6      string * Attrib.src list -> Element.context Locale.element list -> Element.statement ->
     1.7 -    local_theory -> Proof.state
     1.8 +    bool -> local_theory -> Proof.state
     1.9    val theorem_i: string -> Method.text option -> (thm list list -> local_theory -> local_theory) ->
    1.10      string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i ->
    1.11 -    local_theory -> Proof.state
    1.12 +    bool -> local_theory -> Proof.state
    1.13 +  val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
    1.14  end;
    1.15  
    1.16  structure Specification: SPECIFICATION =
    1.17 @@ -244,8 +245,16 @@
    1.18                  [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
    1.19        in ((prems, stmt, facts), goal_ctxt) end);
    1.20  
    1.21 +structure TheoremHook = GenericDataFun
    1.22 +(
    1.23 +  type T = ((bool -> Proof.state -> Proof.state) * stamp) list;
    1.24 +  val empty = [];
    1.25 +  val extend = I;
    1.26 +  fun merge _ type_checks : T = Library.merge (eq_snd op =) type_checks;
    1.27 +);
    1.28 +
    1.29  fun gen_theorem prep_att prep_stmt
    1.30 -    kind before_qed after_qed (name, raw_atts) raw_elems raw_concl lthy0 =
    1.31 +    kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy0 =
    1.32    let
    1.33      val _ = LocalTheory.affirm lthy0;
    1.34      val thy = ProofContext.theory_of lthy0;
    1.35 @@ -280,6 +289,8 @@
    1.36      |> ProofContext.note_thmss_i Thm.assumptionK [((AutoBind.assmsN, []), [(prems, [])])]
    1.37      |> snd
    1.38      |> Proof.theorem_i before_qed after_qed' (map snd stmt)
    1.39 +    |> Library.apply (map (fn (f, _) => f int)
    1.40 +      (TheoremHook.get (Context.Proof goal_ctxt)))
    1.41      |> Proof.refine_insert facts
    1.42    end;
    1.43  
    1.44 @@ -288,6 +299,8 @@
    1.45  val theorem = gen_theorem Attrib.intern_src Locale.read_context_statement_i;
    1.46  val theorem_i = gen_theorem (K I) Locale.cert_context_statement;
    1.47  
    1.48 +fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ()));
    1.49 +
    1.50  end;
    1.51  
    1.52  end;