src/Pure/Isar/local_theory.ML
changeset 25021 8f00edb993bd
parent 24984 952045a8dcf2
child 25026 ecdc1733d3cc
     1.1 --- a/src/Pure/Isar/local_theory.ML	Sat Oct 13 17:16:44 2007 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Oct 13 17:16:44 2007 +0200
     1.3 @@ -25,9 +25,9 @@
     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 * term) * local_theory
     1.8 -  val def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
     1.9 -    local_theory -> (term * (bstring * thm)) * local_theory
    1.10 +    (term * (bstring * thm)) * local_theory
    1.11 +  val define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
    1.12 +    (term * (bstring * thm)) * local_theory
    1.13    val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.14      local_theory -> (bstring * thm list) list * local_theory
    1.15    val type_syntax: declaration -> local_theory -> local_theory
    1.16 @@ -57,9 +57,10 @@
    1.17    axioms: string ->
    1.18      ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
    1.19      -> (term list * (bstring * thm list) list) * local_theory,
    1.20 -  abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * term) * local_theory,
    1.21 -  def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
    1.22 -    local_theory -> (term * (bstring * thm)) * local_theory,
    1.23 +  abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
    1.24 +    (term * (bstring * thm)) * local_theory,
    1.25 +  define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
    1.26 +    (term * (bstring * thm)) * local_theory,
    1.27    notes: string ->
    1.28      ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.29      local_theory -> (bstring * thm list) list * local_theory,
    1.30 @@ -151,7 +152,7 @@
    1.31  val pretty = operation #pretty;
    1.32  val axioms = operation2 #axioms;
    1.33  val abbrev = operation2 #abbrev;
    1.34 -val def = operation2 #def;
    1.35 +val define = operation2 #define;
    1.36  val notes = operation2 #notes;
    1.37  val type_syntax = operation1 #type_syntax;
    1.38  val term_syntax = operation1 #term_syntax;