src/HOL/Library/Bit.thy

   "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
   "HOL.equal 1 b \<longleftrightarrow> set b"
   by (simp_all add: equal set_iff)
 
 
-subsection \<open>Type @{typ bit} forms a field\<close>
+subsection \<open>Type \<^typ>\<open>bit\<close> forms a field\<close>
 
 instantiation bit :: field
 begin
 
 definition plus_bit_def: "x + y = case_bit y (case_bit 1 0 y) x"

 
 lemma bit_add_eq_1_iff: "x + y = 1 \<longleftrightarrow> x \<noteq> y" for x y :: bit
   unfolding plus_bit_def by (simp split: bit.split)
 
 
-subsection \<open>Numerals at type @{typ bit}\<close>
+subsection \<open>Numerals at type \<^typ>\<open>bit\<close>\<close>
 
 text \<open>All numerals reduce to either 0 or 1.\<close>
 
 lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
   by (simp only: uminus_bit_def)

 
 lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
   by (simp only: numeral_Bit1 bit_add_self add_0_left)
 
 
-subsection \<open>Conversion from @{typ bit}\<close>
+subsection \<open>Conversion from \<^typ>\<open>bit\<close>\<close>
 
 context zero_neq_one
 begin
 
 definition of_bit :: "bit \<Rightarrow> 'a"