signature cleanup -- no pervasives anymore;
authorwenzelm
Mon Jun 09 17:07:11 2008 +0200 (2008-06-09)
changeset 270979a6db5d8ee8c
parent 27096 d4145c286bd1
child 27098 d89fb4ee7280
signature cleanup -- no pervasives anymore;
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Jun 09 17:07:10 2008 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Jun 09 17:07:11 2008 +0200
     1.3 @@ -5,38 +5,29 @@
     1.4  Datatype package for Isabelle/HOL.
     1.5  *)
     1.6  
     1.7 -signature BASIC_DATATYPE_PACKAGE =
     1.8 +signature DATATYPE_PACKAGE =
     1.9  sig
    1.10 +  val quiet_mode : bool ref
    1.11 +  val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
    1.12 +  val print_datatypes : theory -> unit
    1.13 +  val get_datatype : theory -> string -> DatatypeAux.datatype_info option
    1.14 +  val the_datatype : theory -> string -> DatatypeAux.datatype_info
    1.15 +  val datatype_of_constr : theory -> string -> DatatypeAux.datatype_info option
    1.16 +  val datatype_of_case : theory -> string -> DatatypeAux.datatype_info option
    1.17 +  val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
    1.18 +  val get_datatype_constrs : theory -> string -> (string * typ) list option
    1.19 +  val construction_interpretation : theory
    1.20 +    -> {atom : typ -> 'a, dtyp : string -> 'a, rtyp : string -> 'a list -> 'a}
    1.21 +    -> (string * sort) list -> string list
    1.22 +    -> (string * (string * 'a list) list) list
    1.23    val induct_tac : string -> int -> tactic
    1.24    val induct_thm_tac : thm -> string -> int -> tactic
    1.25    val case_tac : string -> int -> tactic
    1.26    val distinct_simproc : simproc
    1.27 -end;
    1.28 -
    1.29 -signature DATATYPE_PACKAGE =
    1.30 -sig
    1.31 -  include BASIC_DATATYPE_PACKAGE
    1.32 -  val quiet_mode : bool ref
    1.33 -  val add_datatype_i : bool -> bool -> string list -> (string list * bstring * mixfix *
    1.34 -    (bstring * typ list * mixfix) list) list -> theory ->
    1.35 -      {distinct : thm list list,
    1.36 -       inject : thm list list,
    1.37 -       exhaustion : thm list,
    1.38 -       rec_thms : thm list,
    1.39 -       case_thms : thm list list,
    1.40 -       split_thms : (thm * thm) list,
    1.41 -       induction : thm,
    1.42 -       simps : thm list} * theory
    1.43 -  val add_datatype : bool -> string list -> (string list * bstring * mixfix *
    1.44 -    (bstring * string list * mixfix) list) list -> theory ->
    1.45 -      {distinct : thm list list,
    1.46 -       inject : thm list list,
    1.47 -       exhaustion : thm list,
    1.48 -       rec_thms : thm list,
    1.49 -       case_thms : thm list list,
    1.50 -       split_thms : (thm * thm) list,
    1.51 -       induction : thm,
    1.52 -       simps : thm list} * theory
    1.53 +  val make_case :  Proof.context -> bool -> string list -> term ->
    1.54 +    (term * term) list -> term * (term * (int * bool)) list
    1.55 +  val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
    1.56 +  val interpretation : (string list -> theory -> theory) -> theory -> theory
    1.57    val rep_datatype_i : string list option -> (thm list * attribute list) list list ->
    1.58      (thm list * attribute list) list list -> (thm list * attribute list) ->
    1.59      theory ->
    1.60 @@ -58,23 +49,26 @@
    1.61         split_thms : (thm * thm) list,
    1.62         induction : thm,
    1.63         simps : thm list} * theory
    1.64 -  val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
    1.65 -  val get_datatype : theory -> string -> DatatypeAux.datatype_info option
    1.66 -  val the_datatype : theory -> string -> DatatypeAux.datatype_info
    1.67 -  val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
    1.68 -  val datatype_of_constr : theory -> string -> DatatypeAux.datatype_info option
    1.69 -  val datatype_of_case : theory -> string -> DatatypeAux.datatype_info option
    1.70 -  val get_datatype_constrs : theory -> string -> (string * typ) list option
    1.71 -  val construction_interpretation: theory
    1.72 -    -> { atom: typ -> 'a, dtyp: string -> 'a, rtyp: string -> 'a list -> 'a }
    1.73 -    -> (string * Term.sort) list -> string list
    1.74 -    -> (string * (string * 'a list) list) list
    1.75 -  val interpretation: (string list -> theory -> theory) -> theory -> theory
    1.76 -  val print_datatypes : theory -> unit
    1.77 -  val make_case :  Proof.context -> bool -> string list -> term ->
    1.78 -    (term * term) list -> term * (term * (int * bool)) list
    1.79 -  val strip_case: Proof.context -> bool ->
    1.80 -    term -> (term * (term * term) list) option
    1.81 +  val add_datatype_i : bool -> bool -> string list -> (string list * bstring * mixfix *
    1.82 +    (bstring * typ list * mixfix) list) list -> theory ->
    1.83 +      {distinct : thm list list,
    1.84 +       inject : thm list list,
    1.85 +       exhaustion : thm list,
    1.86 +       rec_thms : thm list,
    1.87 +       case_thms : thm list list,
    1.88 +       split_thms : (thm * thm) list,
    1.89 +       induction : thm,
    1.90 +       simps : thm list} * theory
    1.91 +  val add_datatype : bool -> string list -> (string list * bstring * mixfix *
    1.92 +    (bstring * string list * mixfix) list) list -> theory ->
    1.93 +      {distinct : thm list list,
    1.94 +       inject : thm list list,
    1.95 +       exhaustion : thm list,
    1.96 +       rec_thms : thm list,
    1.97 +       case_thms : thm list list,
    1.98 +       split_thms : (thm * thm) list,
    1.99 +       induction : thm,
   1.100 +       simps : thm list} * theory
   1.101    val setup: theory -> theory
   1.102  end;
   1.103  
   1.104 @@ -831,6 +825,3 @@
   1.105  
   1.106  end;
   1.107  
   1.108 -structure BasicDatatypePackage: BASIC_DATATYPE_PACKAGE = DatatypePackage;
   1.109 -open BasicDatatypePackage;
   1.110 -