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";