Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added proof function declarations for min and max
authorberghofe
Thu, 10 Jan 2013 18:19:13 +0100
changeset 50788 fec14e8fefb8
parent 50787 065c684130ad
child 50813 b6659475b5af
child 50819 5601ae592679
Added proof function declarations for min and max
src/HOL/SPARK/SPARK.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle