diff -r f04b33ce250f -r a4dc62a46ee4 Inductive.ML
--- a/Inductive.ML	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-(*  Title: 	HOL/inductive.ML
-    ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-(Co)Inductive Definitions for HOL
-
-Inductive definitions use least fixedpoints with standard products and sums
-Coinductive definitions use greatest fixedpoints with Quine products and sums
-
-Sums are used only for mutual recursion;
-Products are used only to derive "streamlined" induction rules for relations
-*)
-
-local open Ind_Syntax
-in
-
-fun gen_fp_oper a (X,T,t) = 
-    let val setT = mk_setT T
-    in Const(a, (setT-->setT)-->setT) $ absfree(X, setT, t)  end;
-
-structure Lfp_items =
-  struct
-  val oper	= gen_fp_oper "lfp"
-  val Tarski	= def_lfp_Tarski
-  val induct	= def_induct
-  end;
-
-structure Gfp_items =
-  struct
-  val oper	= gen_fp_oper "gfp"
-  val Tarski	= def_gfp_Tarski
-  val induct	= def_Collect_coinduct
-  end;
-
-end;
-
-
-functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
-  : sig include INTR_ELIM INDRULE end =
-struct
-structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and 
-				    Fp=Lfp_items);
-
-structure Indrule = Indrule_Fun
-    (structure Inductive=Inductive and Intr_elim=Intr_elim);
-
-open Intr_elim Indrule
-end;
-
-
-structure Ind = Add_inductive_def_Fun (Lfp_items);
-
-
-signature INDUCTIVE_STRING =
-  sig
-  val thy_name   : string 		(*name of the new theory*)
-  val srec_tms   : string list		(*recursion terms*)
-  val sintrs     : string list		(*desired introduction rules*)
-  end;
-
-
-(*For upwards compatibility: can be called directly from ML*)
-functor Inductive_Fun
- (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
-   : sig include INTR_ELIM INDRULE end =
-Ind_section_Fun
-   (open Inductive Ind_Syntax
-    val sign = sign_of thy;
-    val rec_tms = map (readtm sign termTVar) srec_tms
-    and intr_tms = map (readtm sign propT) sintrs;
-    val thy = thy |> Ind.add_fp_def_i(rec_tms, intr_tms) 
-                  |> add_thyname thy_name);
-
-
-
-signature COINDRULE =
-  sig
-  val coinduct : thm
-  end;
-
-
-functor CoInd_section_Fun
- (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
-    : sig include INTR_ELIM COINDRULE end =
-struct
-structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp_items);
-
-open Intr_elim 
-val coinduct = raw_induct
-end;
-
-
-structure CoInd = Add_inductive_def_Fun(Gfp_items);