changeset 289 | 78541329ff35 |
parent 226 | cc87161971e4 |
--- a/src/CCL/wfd.ML Tue Mar 22 08:24:14 1994 +0100 +++ b/src/CCL/wfd.ML Tue Mar 22 12:42:56 1994 +0100 @@ -179,7 +179,7 @@ by (fast_tac set_cs 1); val NatPRXH = result(); -goalw Wfd.thy [ListPR_def] "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h.t>)"; +goalw Wfd.thy [ListPR_def] "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)"; by (fast_tac set_cs 1); val ListPRXH = result();