src/Pure/Isar/local_theory.ML
changeset 28083 103d9282a946
parent 28017 4919bd124a58
child 28084 a05ca48ef263
     1.1 --- a/src/Pure/Isar/local_theory.ML	Tue Sep 02 14:10:32 2008 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Tue Sep 02 14:10:45 2008 +0200
     1.3 @@ -26,16 +26,16 @@
     1.4    val affirm: local_theory -> local_theory
     1.5    val pretty: local_theory -> Pretty.T list
     1.6    val axioms: string ->
     1.7 -    ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
     1.8 -    -> (term list * (bstring * thm list) list) * local_theory
     1.9 -  val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
    1.10 +    ((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list -> local_theory
    1.11 +    -> (term list * (string * thm list) list) * local_theory
    1.12 +  val abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
    1.13      (term * term) * local_theory
    1.14 -  val define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
    1.15 -    (term * (bstring * thm)) * local_theory
    1.16 -  val note: string -> (bstring * Attrib.src list) * thm list ->
    1.17 -    local_theory -> (bstring * thm list) * local_theory
    1.18 -  val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.19 -    local_theory -> (bstring * thm list) list * local_theory
    1.20 +  val define: string -> (Name.binding * mixfix) * ((Name.binding * Attrib.src list) * term) -> local_theory ->
    1.21 +    (term * (string * thm)) * local_theory
    1.22 +  val note: string -> (Name.binding * Attrib.src list) * thm list ->
    1.23 +    local_theory -> (string * thm list) * local_theory
    1.24 +  val notes: string -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.25 +    local_theory -> (string * thm list) list * local_theory
    1.26    val type_syntax: declaration -> local_theory -> local_theory
    1.27    val term_syntax: declaration -> local_theory -> local_theory
    1.28    val declaration: declaration -> local_theory -> local_theory
    1.29 @@ -57,15 +57,15 @@
    1.30  type operations =
    1.31   {pretty: local_theory -> Pretty.T list,
    1.32    axioms: string ->
    1.33 -    ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
    1.34 -    -> (term list * (bstring * thm list) list) * local_theory,
    1.35 -  abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * term) * local_theory,
    1.36 +    ((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list -> local_theory
    1.37 +    -> (term list * (string * thm list) list) * local_theory,
    1.38 +  abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory -> (term * term) * local_theory,
    1.39    define: string ->
    1.40 -    (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
    1.41 -    (term * (bstring * thm)) * local_theory,
    1.42 +    (Name.binding * mixfix) * ((Name.binding * Attrib.src list) * term) -> local_theory ->
    1.43 +    (term * (string * thm)) * local_theory,
    1.44    notes: string ->
    1.45 -    ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.46 -    local_theory -> (bstring * thm list) list * local_theory,
    1.47 +    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.48 +    local_theory -> (string * thm list) list * local_theory,
    1.49    type_syntax: declaration -> local_theory -> local_theory,
    1.50    term_syntax: declaration -> local_theory -> local_theory,
    1.51    declaration: declaration -> local_theory -> local_theory,