Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Z2.thy
changeset 75962 c530cb79ccbc
parent 74108 3146646a43a7
child 79072 a91050cd5c93 
--- a/src/HOL/Library/Z2.thy	Mon Aug 22 21:37:06 2022 +0200
+++ b/src/HOL/Library/Z2.thy	Wed Aug 24 06:21:06 2022 +0000
@@ -140,7 +140,7 @@
   \<open>a mod b = of_bool (odd a \<and> even b)\<close> for a b :: bit
   by (simp add: modulo_bit_def Abs_bit_eq_of_bool Rep_bit_eq_odd)
 
-lemma power_bit_unfold [simp, code]:
+lemma power_bit_unfold [simp]:
   \<open>a ^ n = of_bool (odd a \<or> n = 0)\<close> for a :: bit
   by (cases a) simp_all
 
@@ -235,10 +235,12 @@
   by (simp add: fun_eq_iff)
 
 
-lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
+lemma bit_numeral_even [simp]:
+  \<open>numeral (Num.Bit0 n) = (0 :: bit)\<close>
   by (simp only: Z2.bit_eq_iff even_numeral) simp
 
-lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
+lemma bit_numeral_odd [simp]:
+  \<open>numeral (Num.Bit1 n) = (1 :: bit)\<close>
   by (simp only: Z2.bit_eq_iff odd_numeral)  simp
 
 end
isabelle