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/Word/Bits.thy
changeset 71957 3e162c63371a
parent 71149 a7d1fb0c9e16 
--- a/src/HOL/Word/Bits.thy	Thu Jun 18 09:07:30 2020 +0000
+++ b/src/HOL/Word/Bits.thy	Thu Jun 18 09:07:30 2020 +0000
@@ -5,15 +5,11 @@
 section \<open>Syntactic type classes for bit operations\<close>
 
 theory Bits
-  imports Main
+  imports Main "HOL-Library.Bit_Operations"
 begin
 
 class bit_operations =
-  fixes bitNOT :: "'a \<Rightarrow> 'a"  ("NOT")
-    and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "AND" 64)
-    and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "OR"  59)
-    and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "XOR" 59)
-    and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl "<<" 55)
+  fixes shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl "<<" 55)
     and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl ">>" 55)
   fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool"  (infixl "!!" 100)
     and lsb :: "'a \<Rightarrow> bool"
isabelle