1.1 --- a/src/HOL/SPARK/SPARK.thy	Tue Jan 08 22:10:02 2013 +0100
     1.2 +++ b/src/HOL/SPARK/SPARK.thy	Thu Jan 10 18:19:13 2013 +0100
     1.3 @@ -275,4 +275,11 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +
     1.8 +text {* Minimum and maximum *}
     1.9 +
    1.10 +spark_proof_functions
    1.11 +  integer__min = "min :: int \<Rightarrow> int \<Rightarrow> int"
    1.12 +  integer__max = "max :: int \<Rightarrow> int \<Rightarrow> int"
    1.13 +
    1.14  end