src/CCL/Term.thy
changeset 289 78541329ff35
parent 0 a5a9c433f639
child 610 ede55dd46f9d
     1.1 --- a/src/CCL/Term.thy	Tue Mar 22 08:24:14 1994 +0100
     1.2 +++ b/src/CCL/Term.thy	Tue Mar 22 12:42:56 1994 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4    nrec       ::	      "[i,i,[i,i]=>i]=>i"
     1.5  
     1.6    nil        ::       "i"                    ("([])")
     1.7 -  "."        ::       "[i,i]=>i"             (infixr 80)
     1.8 +  "$"        ::       "[i,i]=>i"             (infixr 80)
     1.9    lcase      ::	      "[i,i,[i,i]=>i]=>i"
    1.10    lrec       ::	      "[i,i,[i,i,i]=>i]=>i"
    1.11  
    1.12 @@ -60,7 +60,7 @@
    1.13    ncase_def         "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
    1.14    nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
    1.15    nil_def	              "[] == inl(one)"
    1.16 -  cons_def                   "h.t == inr(<h,t>)"
    1.17 +  cons_def                   "h$t == inr(<h,t>)"
    1.18    lcase_def         "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
    1.19    lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
    1.20