diff -r f04b33ce250f -r a4dc62a46ee4 hologic.ML
--- a/hologic.ML	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,86 +0,0 @@
-(*  Title:      HOL/hologic.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson and Markus Wenzel
-
-Abstract syntax operations for HOL.
-*)
-
-signature HOLOGIC =
-sig
-  val termC: class
-  val termS: sort
-  val termTVar: typ
-  val boolT: typ
-  val mk_setT: typ -> typ
-  val dest_setT: typ -> typ
-  val mk_Trueprop: term -> term
-  val dest_Trueprop: term -> term
-  val conj: term
-  val disj: term
-  val imp: term
-  val eq_const: typ -> term
-  val all_const: typ -> term
-  val exists_const: typ -> term
-  val Collect_const: typ -> term
-  val mk_eq: term * term -> term
-  val mk_all: string * typ * term -> term
-  val mk_exists: string * typ * term -> term
-  val mk_Collect: string * typ * term -> term
-  val mk_mem: term * term -> term
-end;
-
-structure HOLogic: HOLOGIC =
-struct
-
-(* classes *)
-
-val termC: class = "term";
-val termS: sort = [termC];
-
-
-(* types *)
-
-val termTVar = TVar (("'a", 0), termS);
-
-val boolT = Type ("bool", []);
-
-fun mk_setT T = Type ("set", [T]);
-
-fun dest_setT (Type ("set", [T])) = T
-  | dest_setT T = raise_type "dest_setT: set type expected" [T] [];
-
-
-(* terms *)
-
-val Trueprop = Const ("Trueprop", boolT --> propT);
-
-fun mk_Trueprop P = Trueprop $ P;
-
-fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
-  | dest_Trueprop t = raise_term "dest_Trueprop" [t];
-
-
-val conj = Const ("op &", [boolT, boolT] ---> boolT)
-and disj = Const ("op |", [boolT, boolT] ---> boolT)
-and imp = Const ("op -->", [boolT, boolT] ---> boolT);
-
-fun eq_const T = Const ("op =", [T, T] ---> boolT);
-fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
-
-fun all_const T = Const ("All", [T --> boolT] ---> boolT);
-fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
-
-fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
-fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
-
-fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T);
-fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
-
-fun mk_mem (x, A) =
-  let val setT = fastype_of A in
-    Const ("op :", [dest_setT setT, setT] ---> boolT) $ x $ A
-  end;
-
-
-end;
-