Added proof function declarations for min and max
authorberghofe
Thu Jan 10 18:19:13 2013 +0100 (2013-01-10)
changeset 50788fec14e8fefb8
parent 50787 065c684130ad
child 50813 b6659475b5af
child 50819 5601ae592679
Added proof function declarations for min and max
src/HOL/SPARK/SPARK.thy
     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