Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Word/Word.thy
changeset 61824 dcbe9f756ae0
parent 61799 4cf66f21b764
child 61941 31f2105521ee 
--- a/src/HOL/Word/Word.thy	Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/Word/Word.thy	Thu Dec 10 13:38:40 2015 +0000
@@ -3599,7 +3599,7 @@
       apply (simp (no_asm), arith)
      apply (simp (no_asm), arith)
     apply (rule notI [THEN notnotD],
-           drule leI not_leE,
+           drule leI not_le_imp_less,
            drule sbintrunc_inc sbintrunc_dec,      
            simp)+
   done
isabelle