src/HOLCF/Porder.ML
changeset 3018 e65b60b28341
parent 2841 c2508f4ab739
child 3026 7a5611f66b72
--- a/src/HOLCF/Porder.ML	Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOLCF/Porder.ML	Wed Apr 23 11:02:19 1997 +0200
@@ -137,8 +137,8 @@
 
 
 goal thy "lub{x} = x";
-br thelubI 1;
-by(simp_tac (!simpset addsimps [is_lub,is_ub]) 1);
+by (rtac thelubI 1);
+by (simp_tac (!simpset addsimps [is_lub,is_ub]) 1);
 qed "lub_singleton";
 Addsimps [lub_singleton];