src/Pure/Isar/specification.ML
changeset 26336 a0e2b706ce73
parent 25371 26d349416c4f
child 26345 f70620a4cf81
     1.1 --- a/src/Pure/Isar/specification.ML	Wed Mar 19 18:15:25 2008 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Wed Mar 19 22:27:57 2008 +0100
     1.3 @@ -43,10 +43,11 @@
     1.4      local_theory -> local_theory
     1.5    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     1.6    val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
     1.7 -  val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
     1.8 -    -> local_theory -> (bstring * thm list) list * local_theory
     1.9 -  val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
    1.10 -    -> local_theory -> (bstring * thm list) list * local_theory
    1.11 +  val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.12 +    local_theory -> (bstring * thm list) list * local_theory
    1.13 +  val theorems_cmd: string ->
    1.14 +    ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list ->
    1.15 +    local_theory -> (bstring * thm list) list * local_theory
    1.16    val theorem: string -> Method.text option ->
    1.17      (thm list list -> local_theory -> local_theory) ->
    1.18      string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i ->