equal
deleted
inserted
replaced
996 |
996 |
997 lemma xt9 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) > c ==> |
997 lemma xt9 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) > c ==> |
998 (!!x y. x > y ==> f x > f y) ==> f a > c" |
998 (!!x y. x > y ==> f x > f y) ==> f a > c" |
999 by (subgoal_tac "f a > f b", force, force) |
999 by (subgoal_tac "f a > f b", force, force) |
1000 |
1000 |
1001 lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 [no_atp] |
1001 lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 |
1002 |
1002 |
1003 (* |
1003 (* |
1004 Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands |
1004 Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands |
1005 for the wrong thing in an Isar proof. |
1005 for the wrong thing in an Isar proof. |
1006 |
1006 |