src/Pure/Isar/specification.ML
changeset 36317 506d732cb522
parent 36106 19deea200358
child 36323 655e2d74de3a
     1.1 --- a/src/Pure/Isar/specification.ML	Fri Apr 23 22:39:49 2010 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Fri Apr 23 22:48:07 2010 +0200
     1.3 @@ -62,6 +62,14 @@
     1.4      (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
     1.5      Element.context list -> Element.statement ->
     1.6      bool -> local_theory -> Proof.state
     1.7 +  val schematic_theorem: string -> Method.text option ->
     1.8 +    (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
     1.9 +    Element.context_i list -> Element.statement_i ->
    1.10 +    bool -> local_theory -> Proof.state
    1.11 +  val schematic_theorem_cmd: string -> Method.text option ->
    1.12 +    (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
    1.13 +    Element.context list -> Element.statement ->
    1.14 +    bool -> local_theory -> Proof.state
    1.15    val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
    1.16  end;
    1.17  
    1.18 @@ -361,7 +369,7 @@
    1.19    fun merge hooks : T = Library.merge (eq_snd op =) hooks;
    1.20  );
    1.21  
    1.22 -fun gen_theorem prep_att prep_stmt
    1.23 +fun gen_theorem schematic prep_att prep_stmt
    1.24      kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy =
    1.25    let
    1.26      val _ = Local_Theory.affirm lthy;
    1.27 @@ -397,13 +405,18 @@
    1.28      |> snd
    1.29      |> Proof.theorem_i before_qed after_qed' (map snd stmt)
    1.30      |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
    1.31 +    |> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
    1.32 +        error "Illegal schematic goal statement")
    1.33      |> Library.apply (map (fn (f, _) => f int) (rev (TheoremHook.get (Context.Proof goal_ctxt))))
    1.34    end;
    1.35  
    1.36  in
    1.37  
    1.38 -val theorem = gen_theorem (K I) Expression.cert_statement;
    1.39 -val theorem_cmd = gen_theorem Attrib.intern_src Expression.read_statement;
    1.40 +val theorem = gen_theorem false (K I) Expression.cert_statement;
    1.41 +val theorem_cmd = gen_theorem false Attrib.intern_src Expression.read_statement;
    1.42 +
    1.43 +val schematic_theorem = gen_theorem true (K I) Expression.cert_statement;
    1.44 +val schematic_theorem_cmd = gen_theorem true Attrib.intern_src Expression.read_statement;
    1.45  
    1.46  fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ()));
    1.47