src/HOLCF/Porder0.ML
changeset 4423 a129b817b58a
parent 3842 b55686a7b22c
child 5068 fb28eaa07e01
--- a/src/HOLCF/Porder0.ML	Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/Porder0.ML	Tue Dec 16 17:58:03 1997 +0100
@@ -48,5 +48,5 @@
         ]);
 
 goal Porder0.thy "((x::'a::po)=y) = (x << y & y << x)";
-by(fast_tac (HOL_cs addSEs [antisym_less_inverse] addSIs [antisym_less]) 1);
+by (fast_tac (HOL_cs addSEs [antisym_less_inverse] addSIs [antisym_less]) 1);
 qed "po_eq_conv";