src/CCL/Type.thy
changeset 3837 d7f033c74b38
parent 1474 3f7d67927fe2
child 14765 bafb24c150c1
--- a/src/CCL/Type.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Type.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -46,23 +46,23 @@
 
 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)"
+  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)"
+  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)})"
+  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)})"
+  SPLIT_def   "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})"
 
 end