src/CCL/Term.thy
changeset 289 78541329ff35
parent 0 a5a9c433f639
child 610 ede55dd46f9d
--- a/src/CCL/Term.thy	Tue Mar 22 08:24:14 1994 +0100
+++ b/src/CCL/Term.thy	Tue Mar 22 12:42:56 1994 +0100
@@ -28,7 +28,7 @@
   nrec       ::	      "[i,i,[i,i]=>i]=>i"
 
   nil        ::       "i"                    ("([])")
-  "."        ::       "[i,i]=>i"             (infixr 80)
+  "$"        ::       "[i,i]=>i"             (infixr 80)
   lcase      ::	      "[i,i,[i,i]=>i]=>i"
   lrec       ::	      "[i,i,[i,i,i]=>i]=>i"
 
@@ -60,7 +60,7 @@
   ncase_def         "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
   nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
   nil_def	              "[] == inl(one)"
-  cons_def                   "h.t == inr(<h,t>)"
+  cons_def                   "h$t == inr(<h,t>)"
   lcase_def         "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
   lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"