| changeset 54147 | 97a8ff4e4ac9 |
| parent 53216 | ad2e09c30aa8 |
| child 54857 | 5c05f7c5f8ae |
--- a/src/HOL/Orderings.thy Fri Oct 18 10:35:57 2013 +0200 +++ b/src/HOL/Orderings.thy Fri Oct 18 10:43:20 2013 +0200 @@ -998,7 +998,7 @@ (!!x y. x > y ==> f x > f y) ==> f a > c" by (subgoal_tac "f a > f b", force, force) -lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 [no_atp] +lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 (* Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands