src/HOLCF/Porder0.ML
changeset 5068 fb28eaa07e01
parent 4423 a129b817b58a
child 9169 85a47aa21f74
--- a/src/HOLCF/Porder0.ML	Mon Jun 22 17:12:27 1998 +0200
+++ b/src/HOLCF/Porder0.ML	Mon Jun 22 17:13:09 1998 +0200
@@ -47,6 +47,6 @@
         (atac 1)
         ]);
 
-goal Porder0.thy "((x::'a::po)=y) = (x << y & y << x)";
+Goal "((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";