diff -r 000000000000 -r a5a9c433f639 src/CCL/type.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CCL/type.thy	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,73 @@
+(*  Title:      CCL/types.thy
+    ID:         $Id$
+    Author:     Martin Coen
+    Copyright   1993  University of Cambridge
+
+Types in CCL are defined as sets of terms.
+
+*)
+
+Type = Term +
+
+consts
+
+  Subtype       :: "['a set, 'a => o] => 'a set"
+  Bool          :: "i set"
+  Unit          :: "i set"
+  "+"           :: "[i set, i set] => i set"            (infixr 55)
+  Pi            :: "[i set, i => i set] => i set"
+  Sigma         :: "[i set, i => i set] => i set"
+  Nat           :: "i set"
+  List          :: "i set => i set"
+  Lists         :: "i set => i set"
+  ILists        :: "i set => i set"
+  TAll          :: "(i set => i set) => i set"          (binder "TALL " 55)
+  TEx           :: "(i set => i set) => i set"          (binder "TEX " 55)
+  Lift          :: "i set => i set"                     ("(3[_])")
+
+  SPLIT         :: "[i, [i, i] => i set] => i set"
+
+  "@Pi"         :: "[idt, i set, i set] => i set"       ("(3PROD _:_./ _)" [] 60)
+  "@Sigma"      :: "[idt, i set, i set] => i set"       ("(3SUM _:_./ _)" [] 60)
+  "@->"         :: "[i set, i set] => i set"            ("(_ ->/ _)"  [54, 53] 53)
+  "@*"          :: "[i set, i set] => i set"            ("(_ */ _)" [56, 55] 55)
+  "@Subtype"    :: "[idt, 'a set, o] => 'a set"         ("(1{_: _ ./ _})")
+
+translations
+  "PROD x:A. B" => "Pi(A, %x. B)"
+  "SUM x:A. B"  => "Sigma(A, %x. B)"
+  "{x: A. B}"   == "Subtype(A, %x. B)"
+
+rules
+
+  Subtype_def "{x:A.P(x)} == {x.x:A & P(x)}"
+  Unit_def          "Unit == {x.x=one}"
+  Bool_def          "Bool == {x.x=true | x=false}"
+  Plus_def           "A+B == {x. (EX a:A.x=inl(a)) | (EX b:B.x=inr(b))}"
+  Pi_def         "Pi(A,B) == {x.EX b.x=lam x.b(x) & (ALL x:A.b(x):B(x))}"
+  Sigma_def   "Sigma(A,B) == {x.EX a:A.EX b:B(a).x=<a,b>}"
+  Nat_def            "Nat == lfp(% X.Unit + X)"
+  List_def       "List(A) == lfp(% X.Unit + A*X)"
+
+  Lists_def     "Lists(A) == gfp(% X.Unit + A*X)"
+  ILists_def   "ILists(A) == gfp(% X.{} + A*X)"
+
+  Tall_def   "TALL X.B(X) == Inter({X.EX Y.X=B(Y)})"
+  Tex_def     "TEX X.B(X) == Union({X.EX Y.X=B(Y)})"
+  Lift_def           "[A] == A Un {bot}"
+
+  SPLIT_def   "SPLIT(p,B) == Union({A.EX x y.p=<x,y> & A=B(x,y)})"
+
+end
+
+
+ML
+
+val parse_translation =
+  [("@->", ndependent_tr "Pi"),
+   ("@*", ndependent_tr "Sigma")];
+
+val print_translation =
+  [("Pi", dependent_tr' ("@Pi", "@->")),
+   ("Sigma", dependent_tr' ("@Sigma", "@*"))];
+