--- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Tue Apr 29 22:52:15 2014 +0200
+++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Wed Apr 30 15:43:44 2014 +0200
@@ -27,7 +27,7 @@
*}
definition liseq' :: "(nat \<Rightarrow> 'a::linorder) \<Rightarrow> nat \<Rightarrow> nat" where
- "liseq' xs i = Max (card ` (iseq xs (Suc i) \<inter> {is. Max is = i}))"
+ "liseq' xs i = Max (card ` (iseq xs (Suc i) \<inter> {is. Max is = i}))"
lemma iseq_finite: "finite (iseq xs i)"
apply (simp add: iseq_def)
@@ -541,7 +541,7 @@
text {* The verification conditions *}
-spark_open "liseq/liseq_length.siv"
+spark_open "liseq/liseq_length"
spark_vc procedure_liseq_length_5
by (simp_all add: liseq_singleton liseq'_singleton)