src/HOLCF/Lift1.ML

 
 (* ------------------------------------------------------------------------ *)
 (* less_lift is a partial order on type 'a -> 'b                            *)
 (* ------------------------------------------------------------------------ *)
 
-goalw thy [less_lift_def] "(x::'a lift) << x";
+Goalw [less_lift_def] "(x::'a lift) << x";
 by (fast_tac HOL_cs 1);
 qed"refl_less_lift";
 
 val prems = goalw thy [less_lift_def] 
   "[|(x1::'a lift) << x2; x2 << x1|] ==> x1 = x2";