stripped signature
authorhaftmann
Wed Aug 11 15:09:31 2010 +0200 (2010-08-11 ago)
changeset 383772dfd8b7b8274
parent 38376 dc67291d590b
child 38378 0b6fa86110e7
stripped signature
src/Pure/Isar/class_target.ML
src/Pure/Isar/overloading.ML
     1.1 --- a/src/Pure/Isar/class_target.ML	Wed Aug 11 15:09:30 2010 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Wed Aug 11 15:09:31 2010 +0200
     1.3 @@ -7,31 +7,17 @@
     1.4  signature CLASS_TARGET =
     1.5  sig
     1.6    (*classes*)
     1.7 -  val register: class -> class list -> ((string * typ) * (string * typ)) list
     1.8 -    -> sort -> morphism -> morphism -> thm option -> thm option -> thm
     1.9 -    -> theory -> theory
    1.10 -
    1.11    val is_class: theory -> class -> bool
    1.12 -  val base_sort: theory -> class -> sort
    1.13 -  val rules: theory -> class -> thm option * thm
    1.14    val these_params: theory -> sort -> (string * (class * (string * typ))) list
    1.15 -  val these_defs: theory -> sort -> thm list
    1.16 -  val these_operations: theory -> sort
    1.17 -    -> (string * (class * (typ * term))) list
    1.18    val print_classes: theory -> unit
    1.19  
    1.20 -  val begin: class list -> sort -> Proof.context -> Proof.context
    1.21    val init: class -> theory -> Proof.context
    1.22    val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory
    1.23    val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
    1.24    val class_prefix: string -> string
    1.25    val refresh_syntax: class -> Proof.context -> Proof.context
    1.26 -  val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
    1.27  
    1.28    (*instances*)
    1.29 -  val init_instantiation: string list * (string * sort) list * sort
    1.30 -    -> theory -> Proof.context
    1.31 -  val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
    1.32    val instantiation_instance: (local_theory -> local_theory)
    1.33      -> local_theory -> Proof.state
    1.34    val prove_instantiation_instance: (Proof.context -> tactic)
    1.35 @@ -40,19 +26,14 @@
    1.36      -> local_theory -> theory
    1.37    val prove_instantiation_exit_result: (morphism -> 'a -> 'b)
    1.38      -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory
    1.39 -  val conclude_instantiation: local_theory -> local_theory
    1.40 -  val instantiation_param: local_theory -> binding -> string option
    1.41 -  val confirm_declaration: binding -> local_theory -> local_theory
    1.42 -  val pretty_instantiation: local_theory -> Pretty.T
    1.43    val read_multi_arity: theory -> xstring list * xstring list * xstring
    1.44      -> string list * (string * sort) list * sort
    1.45    val type_name: string -> string
    1.46    val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
    1.47    val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
    1.48 +  val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
    1.49  
    1.50    (*subclasses*)
    1.51 -  val register_subclass: class * class -> morphism option -> Element.witness option
    1.52 -    -> morphism -> theory -> theory
    1.53    val classrel: class * class -> theory -> Proof.state
    1.54    val classrel_cmd: xstring * xstring -> theory -> Proof.state
    1.55  
    1.56 @@ -61,7 +42,24 @@
    1.57    val default_intro_tac: Proof.context -> thm list -> tactic
    1.58  end;
    1.59  
    1.60 -structure Class_Target : CLASS_TARGET =
    1.61 +signature PRIVATE_CLASS_TARGET =
    1.62 +sig
    1.63 +  include CLASS_TARGET
    1.64 +  val register: class -> class list -> ((string * typ) * (string * typ)) list
    1.65 +    -> sort -> morphism -> morphism -> thm option -> thm option -> thm
    1.66 +    -> theory -> theory
    1.67 +  val register_subclass: class * class -> morphism option -> Element.witness option
    1.68 +    -> morphism -> theory -> theory
    1.69 +  val base_sort: theory -> class -> sort
    1.70 +  val rules: theory -> class -> thm option * thm
    1.71 +  val these_defs: theory -> sort -> thm list
    1.72 +  val these_operations: theory -> sort
    1.73 +    -> (string * (class * (typ * term))) list
    1.74 +  val begin: class list -> sort -> Proof.context -> Proof.context
    1.75 +  val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
    1.76 +end;
    1.77 +
    1.78 +structure Class_Target: PRIVATE_CLASS_TARGET =
    1.79  struct
    1.80  
    1.81  (** class data **)
     2.1 --- a/src/Pure/Isar/overloading.ML	Wed Aug 11 15:09:30 2010 +0200
     2.2 +++ b/src/Pure/Isar/overloading.ML	Wed Aug 11 15:09:31 2010 +0200
     2.3 @@ -6,14 +6,6 @@
     2.4  
     2.5  signature OVERLOADING =
     2.6  sig
     2.7 -  val init: (string * (string * typ) * bool) list -> theory -> Proof.context
     2.8 -  val conclude: local_theory -> local_theory
     2.9 -  val declare: string * typ -> theory -> term * theory
    2.10 -  val confirm: binding -> local_theory -> local_theory
    2.11 -  val define: bool -> binding -> string * term -> theory -> thm * theory
    2.12 -  val operation: Proof.context -> binding -> (string * bool) option
    2.13 -  val pretty: Proof.context -> Pretty.T
    2.14 -
    2.15    type improvable_syntax
    2.16    val add_improvable_syntax: Proof.context -> Proof.context
    2.17    val map_improvable_syntax: (improvable_syntax -> improvable_syntax)