--- a/src/HOL/SPARK/SPARK.thy Sat Jul 31 23:15:17 2021 +0200
+++ b/src/HOL/SPARK/SPARK.thy Sun Aug 01 10:20:34 2021 +0000
@@ -12,9 +12,9 @@
text \<open>Bitwise logical operators\<close>
spark_proof_functions
- bit__and (integer, integer) : integer = "(AND)"
- bit__or (integer, integer) : integer = "(OR)"
- bit__xor (integer, integer) : integer = "(XOR)"
+ bit__and (integer, integer) : integer = Bit_Operations.and
+ bit__or (integer, integer) : integer = Bit_Operations.or
+ bit__xor (integer, integer) : integer = Bit_Operations.xor
lemmas [simp] =
OR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified]