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/Bit_Comparison.thy
changeset 61799 4cf66f21b764
parent 55210 d1e3b708d74b
child 67120 491fd7f0b5df 
--- a/src/HOL/Word/Bit_Comparison.thy	Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Word/Bit_Comparison.thy	Mon Dec 07 10:38:04 2015 +0100
@@ -137,7 +137,7 @@
       with 3 have "bin BIT bit = 0" by simp
       then have "bin = 0" and "\<not> bit"
         by (auto simp add: Bit_def split: if_splits) arith
-      then show ?thesis using 0 1 `y < 2 ^ n`
+      then show ?thesis using 0 1 \<open>y < 2 ^ n\<close>
         by simp
     next
       case (Suc m)
@@ -170,7 +170,7 @@
       with 3 have "bin BIT bit = 0" by simp
       then have "bin = 0" and "\<not> bit"
         by (auto simp add: Bit_def split: if_splits) arith
-      then show ?thesis using 0 1 `y < 2 ^ n`
+      then show ?thesis using 0 1 \<open>y < 2 ^ n\<close>
         by simp
     next
       case (Suc m)
isabelle