src/HOL/UNITY/Simple/Lift.ML

 
 (*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
   i.e. the trivial disjunction, leading to an asymmetrical proof.*)
 Goal "0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
 by (Clarify_tac 1);
-by (auto_tac (claset(), metric_ss));
+by (force_tac (claset(), metric_ss) 1);
 qed "E_thm16c";
 
 
 (*lift_5*)
 Goal "0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo   \