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