equal
deleted
inserted
replaced
49 (fn prems =>[ |
49 (fn prems =>[ |
50 resolve_tac prems 1, |
50 resolve_tac prems 1, |
51 cut_facts_tac prems 1, |
51 cut_facts_tac prems 1, |
52 fast_tac HOL_cs 1]); |
52 fast_tac HOL_cs 1]); |
53 |
53 |
54 val dist_eqI = prove_goal Porder.thy "~ x << y ==> x ~= y" (fn prems => [ |
54 val dist_eqI = prove_goal Porder.thy "~(x::'a::po) << y ==> x ~= y" (fn prems => [ |
55 rtac rev_contrapos 1, |
55 rtac rev_contrapos 1, |
56 etac (antisym_less_inverse RS conjunct1) 1, |
56 etac (antisym_less_inverse RS conjunct1) 1, |
57 resolve_tac prems 1]); |
57 resolve_tac prems 1]); |
58 |
58 |
59 in |
59 in |