--- a/src/HOL/Word/Word_Miscellaneous.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Word/Word_Miscellaneous.thy Mon Dec 07 10:38:04 2015 +0100
@@ -2,7 +2,7 @@
Author: Miscellaneous
*)
-section {* Miscellaneous lemmas, of at least doubtful value *}
+section \<open>Miscellaneous lemmas, of at least doubtful value\<close>
theory Word_Miscellaneous
imports Main "~~/src/HOL/Library/Bit" Misc_Numeric
@@ -67,7 +67,7 @@
apply (erule y)
done
--- "simplifications for specific word lengths"
+\<comment> "simplifications for specific word lengths"
lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc'
lemmas s2n_ths = n2s_ths [symmetric]