src/Pure/Isar/local_theory.ML
changeset 38308 0e4649095739
parent 37949 48a874444164
child 38381 7d1e2a6831ec
     1.1 --- a/src/Pure/Isar/local_theory.ML	Tue Aug 10 14:06:38 2010 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Tue Aug 10 14:11:28 2010 +0200
     1.3 @@ -30,9 +30,6 @@
     1.4    val standard_morphism: local_theory -> Proof.context -> morphism
     1.5    val target_morphism: local_theory -> morphism
     1.6    val global_morphism: local_theory -> morphism
     1.7 -  val pretty: local_theory -> Pretty.T list
     1.8 -  val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     1.9 -    (term * term) * local_theory
    1.10    val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    1.11      (term * (string * thm)) * local_theory
    1.12    val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
    1.13 @@ -40,8 +37,11 @@
    1.14      local_theory -> (string * thm list) list * local_theory
    1.15    val notes_kind: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    1.16      local_theory -> (string * thm list) list * local_theory
    1.17 +  val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    1.18 +    (term * term) * local_theory
    1.19    val declaration: bool -> declaration -> local_theory -> local_theory
    1.20    val syntax_declaration: bool -> declaration -> local_theory -> local_theory
    1.21 +  val pretty: local_theory -> Pretty.T list
    1.22    val set_defsort: sort -> local_theory -> local_theory
    1.23    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
    1.24    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    1.25 @@ -65,16 +65,16 @@
    1.26  (* type lthy *)
    1.27  
    1.28  type operations =
    1.29 - {pretty: local_theory -> Pretty.T list,
    1.30 -  abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    1.31 -    (term * term) * local_theory,
    1.32 -  define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    1.33 + {define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    1.34      (term * (string * thm)) * local_theory,
    1.35    notes: string ->
    1.36      (Attrib.binding * (thm list * Attrib.src list) list) list ->
    1.37      local_theory -> (string * thm list) list * local_theory,
    1.38 +  abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    1.39 +    (term * term) * local_theory,
    1.40    declaration: bool -> declaration -> local_theory -> local_theory,
    1.41    syntax_declaration: bool -> declaration -> local_theory -> local_theory,
    1.42 +  pretty: local_theory -> Pretty.T list,
    1.43    reinit: local_theory -> local_theory,
    1.44    exit: local_theory -> Proof.context};
    1.45