--- a/src/HOLCF/Lift1.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Lift1.ML Mon Feb 17 10:57:11 1997 +0100
@@ -13,16 +13,18 @@
(* less_lift is a partial order on type 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
-goalw Lift1.thy [less_lift_def] "less_lift x x";
+goalw thy [less_lift_def] "less (x::'a lift) x";
by (fast_tac HOL_cs 1);
qed"refl_less_lift";
-goalw Lift1.thy [less_lift_def]
- "less_lift x1 x2 & less_lift x2 x1 --> x1 = x2";
+val prems = goalw thy [less_lift_def]
+ "[|less (x1::'a lift) x2; less x2 x1|] ==> x1 = x2";
+by (cut_facts_tac prems 1);
by (fast_tac HOL_cs 1);
qed"antisym_less_lift";
-goalw Lift1.thy [less_lift_def]
- "less_lift x1 x2 & less_lift x2 x3 --> less_lift x1 x3";
+val prems = goalw Lift1.thy [less_lift_def]
+ "[|less (x1::'a lift) x2; less x2 x3|] ==> less x1 x3";
+by (cut_facts_tac prems 1);
by (fast_tac HOL_cs 1);
qed"trans_less_lift";