--- 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)
--- 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)
--- 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)
--- 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"
--- 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>
--- 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)
--- 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"
--- 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"
--- 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" |
--- 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 .
--- 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"
--- 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
--- 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)
--- 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
--- 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
--- 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