equal
deleted
inserted
replaced
10 AddIffs [refl_less]; |
10 AddIffs [refl_less]; |
11 |
11 |
12 (* ------------------------------------------------------------------------ *) |
12 (* ------------------------------------------------------------------------ *) |
13 (* minimal fixes least element *) |
13 (* minimal fixes least element *) |
14 (* ------------------------------------------------------------------------ *) |
14 (* ------------------------------------------------------------------------ *) |
15 bind_thm("minimal2UU",allI RS (prove_goal thy "!x::'a::po.uu<<x==>uu=(@u.!y.u<<y)" |
15 bind_thm("minimal2UU",allI RS (prove_goal thy "!x::'a::po. uu<<x==>uu=(@u.!y. u<<y)" |
16 (fn prems => |
16 (fn prems => |
17 [ |
17 [ |
18 (cut_facts_tac prems 1), |
18 (cut_facts_tac prems 1), |
19 (rtac antisym_less 1), |
19 (rtac antisym_less 1), |
20 (etac spec 1), |
20 (etac spec 1), |