--- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Sun Jan 16 15:26:47 2011 +0100
+++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Sun Jan 16 15:31:22 2011 +0100
@@ -161,7 +161,7 @@
with assms have "Max js < i"
by (auto simp add: iseq_def)
with fin assms have "\<forall>j\<in>js. j < i"
- by (simp add: Max_less_iff)
+ by simp
with assms show ?thesis
by (simp add: iseq_def)
qed
--- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy Sun Jan 16 15:26:47 2011 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy Sun Jan 16 15:31:22 2011 +0100
@@ -6,7 +6,6 @@
theory RMD_Specification
imports RMD SPARK
-
begin
(* bit operations *)