src/CCL/wfd.thy
changeset 289 78541329ff35
parent 227 5415c6ad0028
     1.1 --- a/src/CCL/wfd.thy	Tue Mar 22 08:24:14 1994 +0100
     1.2 +++ b/src/CCL/wfd.thy	Tue Mar 22 12:42:56 1994 +0100
     1.3 @@ -30,5 +30,5 @@
     1.4    "ra**rb == {p. EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
     1.5  
     1.6    NatPR_def      "NatPR == {p.EX x:Nat. p=<x,succ(x)>}"
     1.7 -  ListPR_def     "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h.t>}"
     1.8 +  ListPR_def     "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h$t>}"
     1.9  end