src/HOLCF/Porder0.ML

--- a/src/HOLCF/Porder0.ML	Mon Jun 23 11:33:59 1997 +0200
+++ b/src/HOLCF/Porder0.ML	Thu Jun 26 10:42:50 1997 +0200
@@ -47,3 +47,6 @@
         (atac 1)
         ]);
 
+goal Porder0.thy "((x::'a::po)=y) = (x << y & y << x)";
+by(fast_tac (HOL_cs addSEs [antisym_less_inverse] addSIs [antisym_less]) 1);
+qed "po_eq_conv";