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