# HG changeset patch
# User berghofe
# Date 1357838353 -3600
# Node ID fec14e8fefb82752bee7c1d50856ea9f9308e714
# Parent  065c684130ad2de921ea37b4ad744f9f3a653727
Added proof function declarations for min and max

diff -r 065c684130ad -r fec14e8fefb8 src/HOL/SPARK/SPARK.thy
--- a/src/HOL/SPARK/SPARK.thy	Tue Jan 08 22:10:02 2013 +0100
+++ b/src/HOL/SPARK/SPARK.thy	Thu Jan 10 18:19:13 2013 +0100
@@ -275,4 +275,11 @@
   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