src/Pure/Isar/local_theory.ML
changeset 25104 26b9a7db3386
parent 25026 ecdc1733d3cc
child 25120 23fbc38f6432
     1.1 --- a/src/Pure/Isar/local_theory.ML	Fri Oct 19 19:45:31 2007 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Fri Oct 19 20:57:14 2007 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4      ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
     1.5      -> (term list * (bstring * thm list) list) * local_theory
     1.6    val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
     1.7 -    (term * (bstring * thm)) * local_theory
     1.8 +    (term * thm) * local_theory
     1.9    val define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
    1.10      (term * (bstring * thm)) * local_theory
    1.11    val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.12 @@ -57,8 +57,7 @@
    1.13    axioms: string ->
    1.14      ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
    1.15      -> (term list * (bstring * thm list) list) * local_theory,
    1.16 -  abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
    1.17 -    (term * (bstring * thm)) * local_theory,
    1.18 +  abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * thm) * local_theory,
    1.19    define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
    1.20      (term * (bstring * thm)) * local_theory,
    1.21    notes: string ->