--- a/src/HOLCF/Porder.ML Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/Porder.ML Thu Mar 24 13:36:34 1994 +0100
@@ -6,9 +6,9 @@
Lemmas for theory porder.thy
*)
+open Porder0;
open Porder;
-
val box_less = prove_goal Porder.thy
"[| a << b; c << a; b << d|] ==> c << d"
(fn prems =>