| changeset 1267 | bca91b4e1710 |
| parent 1168 | 74be52691d62 |
| child 1277 | caef3601c0b2 |
--- a/src/HOLCF/Lift1.ML Wed Oct 04 13:12:14 1995 +0100 +++ b/src/HOLCF/Lift1.ML Wed Oct 04 14:01:44 1995 +0100 @@ -84,7 +84,7 @@ (rtac refl 1) ]); -val Lift_ss = Cfun_ss addsimps [Ilift1,Ilift2]; +Addsimps [Ilift1,Ilift2]; qed_goalw "less_lift1a" Lift1.thy [less_lift_def,UU_lift_def] "less_lift(UU_lift)(z)"