src/HOL/Word/Word.thy
changeset 61824 dcbe9f756ae0
parent 61799 4cf66f21b764
child 61941 31f2105521ee
     1.1 --- a/src/HOL/Word/Word.thy	Mon Dec 07 10:49:08 2015 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Thu Dec 10 13:38:40 2015 +0000
     1.3 @@ -3599,7 +3599,7 @@
     1.4        apply (simp (no_asm), arith)
     1.5       apply (simp (no_asm), arith)
     1.6      apply (rule notI [THEN notnotD],
     1.7 -           drule leI not_leE,
     1.8 +           drule leI not_le_imp_less,
     1.9             drule sbintrunc_inc sbintrunc_dec,      
    1.10             simp)+
    1.11    done