equal
deleted
inserted
replaced
41 (fn prems =>[ |
41 (fn prems =>[ |
42 resolve_tac prems 1, |
42 resolve_tac prems 1, |
43 cut_facts_tac prems 1, |
43 cut_facts_tac prems 1, |
44 fast_tac HOL_cs 1]); |
44 fast_tac HOL_cs 1]); |
45 |
45 |
46 val dist_eqI = prove_goal Porder.thy "~(x::'a::po) << y ==> x ~= y" (fn prems => [ |
46 val dist_eqI = prove_goal Porder.thy "!!x::'a::po. ~ x << y ==> x ~= y" |
47 rtac rev_contrapos 1, |
47 (fn prems => [ |
48 etac (antisym_less_inverse RS conjunct1) 1, |
48 (blast_tac (claset() addDs [antisym_less_inverse]) 1)]); |
49 resolve_tac prems 1]); |
|
50 (* |
49 (* |
51 infixr 0 y; |
50 infixr 0 y; |
52 val b = 0; |
51 val b = 0; |
53 fun _ y t = by t; |
52 fun _ y t = by t; |
54 fun g defs t = let val sg = sign_of thy; |
53 fun g defs t = let val sg = sign_of thy; |