equal
deleted
inserted
replaced
10 |
10 |
11 (* ------------------------------------------------------------------------ *) |
11 (* ------------------------------------------------------------------------ *) |
12 (* minimal fixes least element *) |
12 (* minimal fixes least element *) |
13 (* ------------------------------------------------------------------------ *) |
13 (* ------------------------------------------------------------------------ *) |
14 Goal "!x::'a::po. uu<<x ==> uu=(@u.!y. u<<y)"; |
14 Goal "!x::'a::po. uu<<x ==> uu=(@u.!y. u<<y)"; |
15 by (blast_tac (claset() addIs [selectI2,antisym_less]) 1); |
15 by (blast_tac (claset() addIs [someI2,antisym_less]) 1); |
16 bind_thm ("minimal2UU", allI RS result()); |
16 bind_thm ("minimal2UU", allI RS result()); |
17 |
17 |
18 (* ------------------------------------------------------------------------ *) |
18 (* ------------------------------------------------------------------------ *) |
19 (* the reverse law of anti--symmetrie of << *) |
19 (* the reverse law of anti--symmetrie of << *) |
20 (* ------------------------------------------------------------------------ *) |
20 (* ------------------------------------------------------------------------ *) |