src/HOL/SPARK/SPARK.thy

     with 3 show ?thesis
       by (simp only: power_BIT mod_BIT int_and_Bits) simp
   qed
 qed
 
+
+text {* Minimum and maximum *}
+
+spark_proof_functions
+  integer__min = "min :: int \<Rightarrow> int \<Rightarrow> int"
+  integer__max = "max :: int \<Rightarrow> int \<Rightarrow> int"
+
 end