| changeset 1277 | caef3601c0b2 |
| parent 1267 | bca91b4e1710 |
| child 1461 | 6bcb44e4d6e5 |
--- a/src/HOLCF/Lift1.ML Mon Oct 09 14:57:55 1995 +0100 +++ b/src/HOLCF/Lift1.ML Tue Oct 10 11:55:45 1995 +0100 @@ -84,7 +84,7 @@ (rtac refl 1) ]); -Addsimps [Ilift1,Ilift2]; +val Lift0_ss = (simpset_of "Cfun3") addsimps [Ilift1,Ilift2]; qed_goalw "less_lift1a" Lift1.thy [less_lift_def,UU_lift_def] "less_lift(UU_lift)(z)"