added add_typedecls;
authorwenzelm
Wed Jul 01 11:20:32 1998 +0200 (1998-07-01)
changeset 5104230cca8452c7
parent 5103 866a281a8c2a
child 5105 0ff5bec04d02
added add_typedecls;
src/HOL/Tools/typedef_package.ML
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Tue Jun 30 20:57:46 1998 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed Jul 01 11:20:32 1998 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  signature TYPEDEF_PACKAGE =
     1.6  sig
     1.7 +  val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
     1.8    val prove_nonempty: cterm -> thm list -> tactic option -> thm
     1.9    val add_typedef: string -> bstring * string list * mixfix ->
    1.10      string -> string list -> thm list -> tactic option -> theory -> theory
    1.11 @@ -18,6 +19,24 @@
    1.12  struct
    1.13  
    1.14  
    1.15 +(** type declarations **)
    1.16 +
    1.17 +fun add_typedecls decls thy =
    1.18 +  let
    1.19 +    val full = Sign.full_name (Theory.sign_of thy);
    1.20 +
    1.21 +    fun arity_of (raw_name, args, mx) =
    1.22 +      (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.termS, HOLogic.termS);
    1.23 +  in
    1.24 +    thy
    1.25 +    |> PureThy.add_typedecls decls
    1.26 +    |> Theory.add_arities_i (map arity_of decls)
    1.27 +  end;
    1.28 +
    1.29 +
    1.30 +
    1.31 +(** type definitions **)
    1.32 +
    1.33  (* prove non-emptyness of a set *)   (*exception ERROR*)
    1.34  
    1.35  val is_def = Logic.is_equals o #prop o rep_thm;