changeset 3323 | 194ae2e0c193 |
parent 2839 | 7ca787c6efca |
child 3326 | 930c9bed5a09 |
--- a/src/HOLCF/Pcpo.ML Fri May 23 18:55:28 1997 +0200 +++ b/src/HOLCF/Pcpo.ML Sun May 25 11:07:52 1997 +0200 @@ -195,7 +195,7 @@ (resolve_tac prems 1) ]); -qed_goal "not_less2not_eq" thy "~x<<y ==> ~x=y" +qed_goal "not_less2not_eq" thy "~(x::'a::po)<<y ==> ~x=y" (fn prems => [ (cut_facts_tac prems 1),