src/CCL/Wfd.ML
changeset 289 78541329ff35
parent 226 cc87161971e4
child 642 0db578095e6a
     1.1 --- a/src/CCL/Wfd.ML	Tue Mar 22 08:24:14 1994 +0100
     1.2 +++ b/src/CCL/Wfd.ML	Tue Mar 22 12:42:56 1994 +0100
     1.3 @@ -179,7 +179,7 @@
     1.4  by (fast_tac set_cs 1);
     1.5  val NatPRXH = result();
     1.6  
     1.7 -goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h.t>)";
     1.8 +goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)";
     1.9  by (fast_tac set_cs 1);
    1.10  val ListPRXH = result();
    1.11