Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
corrected operation
authorhaftmann
Tue, 15 Apr 2025 19:40:42 +0200
changeset 82515 03d019ee7d02
parent 82514 efc1cd044440
child 82516 88f101c3cfe2
corrected operation
src/HOL/Code_Numeral.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Code_Numeral.thy	Tue Apr 15 19:40:39 2025 +0200
+++ b/src/HOL/Code_Numeral.thy	Tue Apr 15 19:40:42 2025 +0200
@@ -642,7 +642,7 @@
   by (transfer; simp)+
 
 lemma or_integer_code [code]:
-  \<open>Pos Num.One AND Pos Num.One = Pos Num.One\<close>
+  \<open>Pos Num.One OR Pos Num.One = Pos Num.One\<close>
   \<open>Pos Num.One OR Pos (Num.Bit0 n) = Pos (Num.Bit1 n)\<close>
   \<open>Pos (Num.Bit0 m) OR Pos Num.One = Pos (Num.Bit1 m)\<close>
   \<open>Pos Num.One OR Pos (Num.Bit1 n) = Pos (Num.Bit1 n)\<close>
isabelle