--- a/src/CCL/Hered.ML Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/Hered.ML Tue Mar 22 12:42:56 1994 +0100
@@ -70,7 +70,7 @@
"zero : HTT",
"succ(n) : HTT <-> n : HTT",
"[] : HTT",
- "x.xs : HTT <-> x : HTT & xs : HTT"];
+ "x$xs : HTT <-> x : HTT & xs : HTT"];
end;
val HTT_Is = HTT_rews @ (HTT_rews RL [iffD2]);
@@ -108,7 +108,7 @@
\ succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
"[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
"[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==>\
-\ h.t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"];
+\ h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"];
(*** Formation Rules for Types ***)