# HG changeset patch
# User wenzelm
# Date 1515767266 -3600
# Node ID 4a4c14b2480084ad4f0da12450548822d67030b9
# Parent  dbaa38bd223a380e8cd3fe22bf35c2a42884a552
prefer formal comments;

diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
--- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -357,7 +357,7 @@
 by (blast intro: ChainsI dest: in_ChainsD)
 
 lemma fixp_above_Kleene_iter:
-  assumes "\<forall>M \<in> Chains leq. finite M" (* convenient but surely not necessary *)
+  assumes "\<forall>M \<in> Chains leq. finite M"  \<comment> \<open>convenient but surely not necessary\<close>
   assumes "(f ^^ Suc k) a = (f ^^ k) a"
   shows "fixp_above a = (f ^^ k) a"
 proof(rule leq_antisym)
diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/DAList_Multiset.thy
--- a/src/HOL/Library/DAList_Multiset.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Library/DAList_Multiset.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -372,8 +372,7 @@
 
 end
 
-(* we cannot use (\<lambda>a n. (+) (a * n)) for folding, since * is not defined
-   in comm_monoid_add *)
+\<comment> \<open>we cannot use \<open>\<lambda>a n. (+) (a * n)\<close> for folding, since \<open>( * )\<close> is not defined in \<open>comm_monoid_add\<close>\<close>
 lemma sum_mset_Bag[code]: "sum_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (((+) a) ^^ n)) 0 ms"
   unfolding sum_mset.eq_fold
   apply (rule comp_fun_commute.DAList_Multiset_fold)
@@ -381,8 +380,7 @@
   apply (auto simp: ac_simps)
   done
 
-(* we cannot use (\<lambda>a n. ( * ) (a ^ n)) for folding, since ^ is not defined
-   in comm_monoid_mult *)
+\<comment> \<open>we cannot use \<open>\<lambda>a n. ( * ) (a ^ n)\<close> for folding, since \<open>(^)\<close> is not defined in \<open>comm_monoid_mult\<close>\<close>
 lemma prod_mset_Bag[code]: "prod_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. ((( * ) a) ^^ n)) 1 ms"
   unfolding prod_mset.eq_fold
   apply (rule comp_fun_commute.DAList_Multiset_fold)
diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -181,7 +181,7 @@
     by (intro cSUP_upper bdd_above_image_mono assms) (auto simp: mono_def)
 qed
 
-(*These generalise their counterparts in Nat.linordered_semidom_class*)
+\<comment> \<open>These generalise their counterparts in \<open>Nat.linordered_semidom_class\<close>\<close>
 lemma of_nat_less[simp]:
   "m < n \<Longrightarrow> of_nat m < (of_nat n::'a::{linordered_nonzero_semiring, semiring_char_0})"
   by (auto simp: less_le)
diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -4091,7 +4091,7 @@
 
 subsubsection \<open>Tests for code generator\<close>
 
-(* A small list of simple arithmetic expressions *)
+text \<open>A small list of simple arithmetic expressions.\<close>
 
 value "- \<infinity> :: ereal"
 value "\<bar>-\<infinity>\<bar> :: ereal"
diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Library/FSet.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -1204,7 +1204,7 @@
 
 subsection \<open>Advanced relator customization\<close>
 
-(* Set vs. sum relators: *)
+text \<open>Set vs. sum relators:\<close>
 
 lemma rel_set_rel_sum[simp]:
 "rel_set (rel_sum \<chi> \<phi>) A1 A2 \<longleftrightarrow>
diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -188,7 +188,7 @@
 lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
   by (simp add: cofinite_eq_sequentially)
 
-(* legacy names *)
+\<comment> \<open>legacy names\<close>
 lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
 lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp
 lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -28,7 +28,8 @@
 
 section\<open>Linear temporal logic\<close>
 
-(* Propositional connectives: *)
+text \<open>Propositional connectives:\<close>
+
 abbreviation (input) IMPL (infix "impl" 60)
 where "\<phi> impl \<psi> \<equiv> \<lambda> xs. \<phi> xs \<longrightarrow> \<psi> xs"
 
@@ -55,7 +56,8 @@
 
 lemma non_not[simp]: "not (not \<phi>) = \<phi>" by simp
 
-(* Temporal (LTL) connectives: *)
+text \<open>Temporal (LTL) connectives:\<close>
+
 fun holds where "holds P xs \<longleftrightarrow> P (shd xs)"
 fun nxt where "nxt \<phi> xs = \<phi> (stl xs)"
 
@@ -76,7 +78,7 @@
 coinductive alw for \<phi> where
 alw: "\<lbrakk>\<phi> xs; alw \<phi> (stl xs)\<rbrakk> \<Longrightarrow> alw \<phi> xs"
 
-(* weak until: *)
+\<comment> \<open>weak until:\<close>
 coinductive UNTIL (infix "until" 60) for \<phi> \<psi> where
 base: "\<psi> xs \<Longrightarrow> (\<phi> until \<psi>) xs"
 |
@@ -377,7 +379,7 @@
   thus ?L by (induct rule: sset_induct) (simp_all add: ev.base ev.step)
 qed
 
-(* LTL as a program logic: *)
+text \<open>LTL as a program logic:\<close>
 lemma alw_invar:
 assumes "\<phi> xs" and "alw (\<phi> impl nxt \<phi>) xs"
 shows "alw \<phi> xs"
diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Library/Permutations.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -1054,7 +1054,7 @@
   qed
 qed
 
-(* Prove image_mset_eq_implies_permutes *)
+\<comment> \<open>Prove \<open>image_mset_eq_implies_permutes\<close> ...\<close>
 lemma image_mset_eq_implies_permutes:
   fixes f :: "'a \<Rightarrow> 'b"
   assumes "finite A"
@@ -1114,7 +1114,7 @@
 lemma mset_set_upto_eq_mset_upto: "mset_set {..<n} = mset [0..<n]"
   by (induct n) (auto simp: add.commute lessThan_Suc)
 
-(* and derive the existing property: *)
+\<comment> \<open>... and derive the existing property:\<close>
 lemma mset_eq_permutation:
   fixes xs ys :: "'a list"
   assumes mset_eq: "mset xs = mset ys"
diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Library/RBT_Impl.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -1081,8 +1081,7 @@
   "fold f (Branch c lt k v rt) x = fold f rt (f k v (fold f lt x))"
 by(simp_all)
 
-(* fold with continuation predicate *)
-
+\<comment> \<open>fold with continuation predicate\<close>
 fun foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" 
   where
   "foldi c f Empty s = s" |
diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Library/RBT_Set.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -126,14 +126,15 @@
 
 subsection \<open>folding over non empty trees and selecting the minimal and maximal element\<close>
 
-(** concrete **)
+subsubsection \<open>concrete\<close>
 
-(* The concrete part is here because it's probably not general enough to be moved to RBT_Impl *)
+text \<open>The concrete part is here because it's probably not general enough to be moved to \<open>RBT_Impl\<close>\<close>
 
 definition rbt_fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a" 
   where "rbt_fold1_keys f t = List.fold f (tl(RBT_Impl.keys t)) (hd(RBT_Impl.keys t))"
 
-(* minimum *)
+
+paragraph \<open>minimum\<close>
 
 definition rbt_min :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a" 
   where "rbt_min t = rbt_fold1_keys min t"
@@ -229,7 +230,8 @@
       Min.set_eq_fold [symmetric] Min_eqI rbt_min_opt_in_set)
 qed
 
-(* maximum *)
+
+paragraph \<open>maximum\<close>
 
 definition rbt_max :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a" 
   where "rbt_max t = rbt_fold1_keys max t"
@@ -331,7 +333,7 @@
 qed
 
 
-(** abstract **)
+subsubsection \<open>abstract\<close>
 
 context includes rbt.lifting begin
 lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
@@ -351,7 +353,8 @@
     by (auto simp: fold1_keys_def_alt set_keys fold_def_alt non_empty_keys set_eq_fold [symmetric])
 qed
 
-(* minimum *)
+
+paragraph \<open>minimum\<close>
 
 lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min .
 
@@ -388,7 +391,8 @@
     done
 qed
 
-(* maximum *)
+
+paragraph \<open>maximum\<close>
 
 lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max .
 
diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/Stream.thy
--- a/src/HOL/Library/Stream.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Library/Stream.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -21,7 +21,7 @@
 context
 begin
 
-(*for code generation only*)
+\<comment> \<open>for code generation only\<close>
 qualified definition smember :: "'a \<Rightarrow> 'a stream \<Rightarrow> bool" where
   [code_abbrev]: "smember x s \<longleftrightarrow> x \<in> sset s"
 
diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Word/Bits_Int.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -609,7 +609,7 @@
     apply (auto simp: Bit_B0_2t [symmetric])
   done
 
-(*for use when simplifying with bin_nth_Bit*)
+\<comment> \<open>for use when simplifying with \<open>bin_nth_Bit\<close>\<close>
 lemma ex_eq_or: "(\<exists>m. n = Suc m \<and> (m = k \<or> P m)) \<longleftrightarrow> n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m)"
   by auto
 
diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -839,7 +839,7 @@
 lemmas rsplit_aux_simp1s = rsplit_aux_simps [THEN th_if_simp1]
 
 lemmas rsplit_aux_simp2ls = rsplit_aux_simps [THEN th_if_simp2]
-(* these safe to [simp add] as require calculating m - n *)
+\<comment> \<open>these safe to \<open>[simp add]\<close> as require calculating \<open>m - n\<close>\<close>
 lemmas bin_rsplit_aux_simp2s [simp] = rsplit_aux_simp2ls [unfolded Let_def]
 lemmas rbscl = bin_rsplit_aux_simp2s (2)
 
diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Word/Misc_Typedef.thy
--- a/src/HOL/Word/Misc_Typedef.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Word/Misc_Typedef.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -147,15 +147,16 @@
 lemma fns5: "Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> fr \<circ> norm = fr \<and> norm \<circ> fr = fr"
   by (fold eq_norm') auto
 
-(* following give conditions for converses to td_fns1
-  the condition (norm \<circ> fr \<circ> norm = fr \<circ> norm) says that
-  fr takes normalised arguments to normalised results,
-  (norm \<circ> fr \<circ> norm = norm \<circ> fr) says that fr
-  takes norm-equivalent arguments to norm-equivalent results,
-  (fr \<circ> norm = fr) says that fr
-  takes norm-equivalent arguments to the same result, and
-  (norm \<circ> fr = fr) says that fr takes any argument to a normalised result
-  *)
+text \<open>
+  following give conditions for converses to \<open>td_fns1\<close>
+  \<^item> the condition \<open>norm \<circ> fr \<circ> norm = fr \<circ> norm\<close> says that
+    \<open>fr\<close> takes normalised arguments to normalised results
+  \<^item> \<open>norm \<circ> fr \<circ> norm = norm \<circ> fr\<close> says that \<open>fr\<close>
+    takes norm-equivalent arguments to norm-equivalent results
+  \<^item> \<open>fr \<circ> norm = fr\<close> says that \<open>fr\<close>
+    takes norm-equivalent arguments to the same result
+  \<^item> \<open>norm \<circ> fr = fr\<close> says that \<open>fr\<close> takes any argument to a normalised result
+\<close>
 lemma fns2: "Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> norm \<circ> fr \<circ> norm = fr \<circ> norm \<longleftrightarrow> Rep \<circ> fa = fr \<circ> Rep"
   apply (fold eq_norm')
   apply safe
diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Word/Word.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -527,10 +527,12 @@
          2 ^ (len_of TYPE('a) - 1))"
   using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2)
 
-(* We do sint before sbin, before sint is the user version
-   and interpretations do not produce thm duplicates. I.e.
-   we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD,
-   because the latter is the same thm as the former *)
+text \<open>
+  We do \<open>sint\<close> before \<open>sbin\<close>, before \<open>sint\<close> is the user version
+  and interpretations do not produce thm duplicates. I.e.
+  we get the name \<open>word_sint.Rep_eqD\<close>, but not \<open>word_sbin.Req_eqD\<close>,
+  because the latter is the same thm as the former.
+\<close>
 interpretation word_sint:
   td_ext
     "sint ::'a::len word \<Rightarrow> int"
@@ -765,7 +767,7 @@
   apply (auto simp add: nth_sbintr)
   done
 
-(* type definitions theorem for in terms of equivalent bool list *)
+\<comment> \<open>type definitions theorem for in terms of equivalent bool list\<close>
 lemma td_bl:
   "type_definition
     (to_bl :: 'a::len0 word \<Rightarrow> bool list)
@@ -862,7 +864,7 @@
   for x :: "'a::len0 word"
   by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])
 
-(* naturals *)
+\<comment> \<open>naturals\<close>
 lemma uints_unats: "uints n = int ` unats n"
   apply (unfold unats_def uints_num)
   apply safe
@@ -898,8 +900,10 @@
     word_of_int (sbintrunc (len_of TYPE('a::len) - 1) (numeral x))"
   by (simp only: word_sbin.Abs_norm word_numeral_alt)
 
-(** cast - note, no arg for new length, as it's determined by type of result,
-  thus in "cast w = w, the type means cast to length of w! **)
+text \<open>
+  \<open>cast\<close> -- note, no arg for new length, as it's determined by type of result,
+  thus in \<open>cast w = w\<close>, the type means cast to length of \<open>w\<close>!
+\<close>
 
 lemma ucast_id: "ucast w = w"
   by (auto simp: ucast_def)
@@ -914,8 +918,7 @@
   by (simp add: ucast_def test_bit_bin word_ubin.eq_norm nth_bintr word_size)
     (fast elim!: bin_nth_uint_imp)
 
-(* for literal u(s)cast *)
-
+\<comment> \<open>literal u(s)cast\<close>
 lemma ucast_bintr [simp]:
   "ucast (numeral w :: 'a::len0 word) =
     word_of_int (bintrunc (len_of TYPE('a)) (numeral w))"
@@ -1171,7 +1174,7 @@
 lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1"
   by (simp add: ucast_def)
 
-(* now, to get the weaker results analogous to word_div/mod_def *)
+\<comment> \<open>now, to get the weaker results analogous to \<open>word_div\<close>/\<open>mod_def\<close>\<close>
 
 
 subsection \<open>Transferring goals from words to ints\<close>
@@ -1244,7 +1247,7 @@
   "word_succ (- 1) = 0 \<and> word_succ 0 = 1 \<and> word_pred 0 = - 1 \<and> word_pred 1 = 0"
   by (simp_all add: word_succ_p1 word_pred_m1)
 
-(* alternative approach to lifting arithmetic equalities *)
+\<comment> \<open>alternative approach to lifting arithmetic equalities\<close>
 lemma word_of_int_Ex: "\<exists>y. x = word_of_int y"
   by (rule_tac x="uint x" in exI) simp
 
@@ -1421,11 +1424,11 @@
   word_uint.Rep_inject [symmetric]
   uint_sub_if' uint_plus_if'
 
-(* use this to stop, eg, 2 ^ len_of TYPE(32) being simplified *)
+\<comment> \<open>use this to stop, eg. \<open>2 ^ len_of TYPE(32)\<close> being simplified\<close>
 lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d"
   by auto
 
-(* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *)
+\<comment> \<open>\<open>uint_arith_tac\<close>: reduce to arithmetic on int, try to solve by arith\<close>
 ML \<open>
 fun uint_arith_simpset ctxt =
   ctxt addsimps @{thms uint_arith_simps}
@@ -1641,7 +1644,7 @@
   apply simp
   done
 
-(* links with rbl operations *)
+\<comment> \<open>links with \<open>rbl\<close> operations\<close>
 lemma word_succ_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = rev (rbl_succ (rev bl))"
   apply (unfold word_succ_def)
   apply clarify
@@ -1690,8 +1693,10 @@
 lemma word_of_int_nat: "0 \<le> x \<Longrightarrow> word_of_int x = of_nat (nat x)"
   by (simp add: word_of_int)
 
-(* note that iszero_def is only for class comm_semiring_1_cancel,
-   which requires word length >= 1, ie 'a::len word *)
+text \<open>
+  note that \<open>iszero_def\<close> is only for class \<open>comm_semiring_1_cancel\<close>,
+  which requires word length \<open>\<ge> 1\<close>, ie \<open>'a::len word\<close>
+\<close>
 lemma iszero_word_no [simp]:
   "iszero (numeral bin :: 'a::len word) =
     iszero (bintrunc (len_of TYPE('a)) (numeral bin))"
@@ -1907,8 +1912,7 @@
   word_unat.Rep_inject [symmetric]
   unat_sub_if' unat_plus_if' unat_div unat_mod
 
-(* unat_arith_tac: tactic to reduce word arithmetic to nat,
-   try to solve via arith *)
+\<comment> \<open>\<open>unat_arith_tac\<close>: tactic to reduce word arithmetic to \<open>nat\<close>, try to solve via \<open>arith\<close>\<close>
 ML \<open>
 fun unat_arith_simpset ctxt =
   ctxt addsimps @{thms unat_arith_simps}
@@ -2087,14 +2091,13 @@
 
 lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
 
-(* following definitions require both arithmetic and bit-wise word operations *)
-
-(* to get word_no_log_defs from word_log_defs, using bin_log_bintrs *)
+\<comment> \<open>following definitions require both arithmetic and bit-wise word operations\<close>
+
+\<comment> \<open>to get \<open>word_no_log_defs\<close> from \<open>word_log_defs\<close>, using \<open>bin_log_bintrs\<close>\<close>
 lemmas wils1 = bin_log_bintrs [THEN word_ubin.norm_eq_iff [THEN iffD1],
   folded word_ubin.eq_norm, THEN eq_reflection]
 
-(* the binary operations only *)
-(* BH: why is this needed? *)
+\<comment> \<open>the binary operations only\<close>  (* BH: why is this needed? *)
 lemmas word_log_binary_defs =
   word_and_def word_or_def word_xor_def
 
@@ -2201,9 +2204,7 @@
 lemma nth_minus1 [simp]: "(-1 :: 'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
   by transfer simp
 
-(* get from commutativity, associativity etc of int_and etc
-  to same for word_and etc *)
-
+\<comment> \<open>get from commutativity, associativity etc of \<open>int_and\<close> etc to same for \<open>word_and etc\<close>\<close>
 lemmas bwsimps =
   wi_hom_add
   word_wi_log_defs
@@ -2670,9 +2671,11 @@
    apply (auto simp add: nth_shiftr1)
   done
 
-(* see paper page 10, (1), (2), shiftr1_def is of the form of (1),
-  where f (ie bin_rest) takes normal arguments to normal results,
-  thus we get (2) from (1) *)
+text \<open>
+  see paper page 10, (1), (2), \<open>shiftr1_def\<close> is of the form of (1),
+  where \<open>f\<close> (ie \<open>bin_rest\<close>) takes normal arguments to normal results,
+  thus we get (2) from (1)
+\<close>
 
 lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)"
   apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i)
@@ -2774,7 +2777,7 @@
   for w :: "'a::len word"
   by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') (fast intro!: Suc_leI)
 
-(* Generalized version of bl_shiftl1. Maybe this one should replace it? *)
+\<comment> \<open>Generalized version of \<open>bl_shiftl1\<close>. Maybe this one should replace it?\<close>
 lemma bl_shiftl1': "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
   by (simp add: shiftl1_bl word_rep_drop drop_Suc del: drop_append)
 
@@ -2788,7 +2791,7 @@
   for w :: "'a::len word"
   by (simp add: shiftr1_bl word_rep_drop len_gt_0 [THEN Suc_leI])
 
-(* Generalized version of bl_shiftr1. Maybe this one should replace it? *)
+\<comment> \<open>Generalized version of \<open>bl_shiftr1\<close>. Maybe this one should replace it?\<close>
 lemma bl_shiftr1': "to_bl (shiftr1 w) = butlast (False # to_bl w)"
   apply (rule word_bl.Abs_inverse')
    apply (simp del: butlast.simps)
@@ -2909,7 +2912,7 @@
   apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
   done
 
-(* note - the following results use 'a::len word < number_ring *)
+\<comment> \<open>note -- the following results use \<open>'a::len word < number_ring\<close>\<close>
 
 lemma shiftl1_2t: "shiftl1 w = 2 * w"
   for w :: "'a::len word"
@@ -3719,7 +3722,7 @@
 
 lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
 
-(* alternative proof of word_rcat_rsplit *)
+\<comment> \<open>alternative proof of \<open>word_rcat_rsplit\<close>\<close>
 lemmas tdle = times_div_less_eq_dividend
 lemmas dtle = xtr4 [OF tdle mult.commute]
 
@@ -4047,7 +4050,7 @@
 
 subsubsection \<open>"Word rotation commutes with bit-wise operations\<close>
 
-(* using locale to not pollute lemma namespace *)
+\<comment> \<open>using locale to not pollute lemma namespace\<close>
 locale word_rotate
 begin
 
diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Word/Word_Miscellaneous.thy
--- a/src/HOL/Word/Word_Miscellaneous.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -95,8 +95,7 @@
 lemma if_same_eq_not: "(If p x y = (\<not> If p u v)) = (if p then x = (\<not> u) else y = (\<not> v))"
   by auto
 
-(* note - if_Cons can cause blowup in the size, if p is complex,
-  so make a simproc *)
+\<comment> \<open>note -- \<open>if_Cons\<close> can cause blowup in the size, if \<open>p\<close> is complex, so make a simproc\<close>
 lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys"
   by auto