src/HOL/typedef.ML

--- a/src/HOL/typedef.ML	Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/typedef.ML	Mon Feb 05 21:27:16 1996 +0100
@@ -1,20 +1,20 @@
-(*  Title:      HOL/subtype.ML
+(*  Title:      HOL/typedef.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Internal interface for subtype definitions.
+Internal interface for typedef definitions.
 *)
 
-signature SUBTYPE =
+signature TYPEDEF =
 sig
   val prove_nonempty: cterm -> thm list -> tactic option -> thm
-  val add_subtype: string -> string * string list * mixfix ->
+  val add_typedef: string -> string * string list * mixfix ->
     string -> string list -> thm list -> tactic option -> theory -> theory
-  val add_subtype_i: string -> string * string list * mixfix ->
+  val add_typedef_i: string -> string * string list * mixfix ->
     term -> string list -> thm list -> tactic option -> theory -> theory
 end;
 
-structure Subtype: SUBTYPE =
+structure Typedef: TYPEDEF =
 struct
 
 open Syntax Logic HOLogic;
@@ -41,11 +41,11 @@
     error ("Failed to prove non-emptyness of " ^ quote (string_of_cterm cset));
 
 
-(* ext_subtype *)
+(* ext_typedef *)
 
-fun ext_subtype prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
+fun ext_typedef prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
   let
-    val dummy = require_thy thy "Set" "subtype definitions";
+    val dummy = require_thy thy "Set" "typedef definitions";
     val sign = sign_of thy;
 
     (*rhs*)
@@ -122,7 +122,7 @@
       (Abs_name ^ "_inverse", abs_type_inv)]
   end
   handle ERROR =>
-    error ("The error(s) above occurred in subtype definition " ^ quote name);
+    error ("The error(s) above occurred in typedef definition " ^ quote name);
 
 
 (* external interfaces *)
@@ -133,8 +133,8 @@
 fun read_term sg str =
   read_cterm sg (str, termTVar);
 
-val add_subtype = ext_subtype read_term;
-val add_subtype_i = ext_subtype cert_term;
+val add_typedef = ext_typedef read_term;
+val add_typedef_i = ext_typedef cert_term;
 
 
 end;