src/HOL/Word/Bool_List_Representation.thy

 lemma map2_Cons [simp, code]:
   "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys"
   unfolding map2_def by auto
 
 
-subsection {* Operations on lists of booleans *}
+subsection \<open>Operations on lists of booleans\<close>
 
 primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
 where
   Nil: "bl_to_bin_aux [] w = w"
   | Cons: "bl_to_bin_aux (b # bs) w = 

         | y # ys => y # takefill fill n ys)"
 
 
 subsection "Arithmetic in terms of bool lists"
 
-text {* 
+text \<open>
   Arithmetic operations in terms of the reversed bool list,
   assuming input list(s) the same length, and don't extend them. 
-*}
+\<close>
 
 primrec rbl_succ :: "bool list => bool list"
 where
   Nil: "rbl_succ Nil = Nil"
   | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"

   Nil: "rbl_pred Nil = Nil"
   | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
 
 primrec rbl_add :: "bool list => bool list => bool list"
 where
-  -- "result is length of first arg, second arg may be longer"
+  \<comment> "result is length of first arg, second arg may be longer"
   Nil: "rbl_add Nil x = Nil"
   | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in 
     (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
 
 primrec rbl_mult :: "bool list => bool list => bool list"
 where
-  -- "result is length of first arg, second arg may be longer"
+  \<comment> "result is length of first arg, second arg may be longer"
   Nil: "rbl_mult Nil x = Nil"
   | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in 
     if y then rbl_add ws x else ws)"
 
 lemma butlast_power:

 lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
   "0 < n ==> bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = 
     bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
   by (cases n) auto
 
-text {* Link between bin and bool list. *}
+text \<open>Link between bin and bool list.\<close>
 
 lemma bl_to_bin_aux_append: 
   "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
   by (induct bs arbitrary: w) auto
 

     length (bin_rsplit_aux n nw v bs) =
     length (bin_rsplit_aux n nw w cs)"
 proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct)
   case (1 n m w cs v bs) show ?case
   proof (cases "m = 0")
-    case True then show ?thesis using `length bs = length cs` by simp
+    case True then show ?thesis using \<open>length bs = length cs\<close> by simp
   next
     case False
-    from "1.hyps" `m \<noteq> 0` `n \<noteq> 0` have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
+    from "1.hyps" \<open>m \<noteq> 0\<close> \<open>n \<noteq> 0\<close> have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
       length (bin_rsplit_aux n (m - n) v bs) =
       length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))"
     by auto
-    show ?thesis using `length bs = length cs` `n \<noteq> 0`
+    show ?thesis using \<open>length bs = length cs\<close> \<open>n \<noteq> 0\<close>
       by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len
         split: prod.split)
   qed
 qed
 

   apply (erule bin_rsplit_aux_len_indep)
   apply (rule refl)
   done
 
 
-text {* Even more bit operations *}
+text \<open>Even more bit operations\<close>
 
 instantiation int :: bitss
 begin
 
 definition [iff]: