# HG changeset patch # User wenzelm # Date 1295188282 -3600 # Node ID 9546828c0eb3ec2c9b4ae234efa491b95ce01dc6 # Parent e13df75fee79d7e49c4f47d1c873d1b3eccf17ba tuned; diff -r e13df75fee79 -r 9546828c0eb3 src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy --- 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 "\j\js. j < i" - by (simp add: Max_less_iff) + by simp with assms show ?thesis by (simp add: iseq_def) qed diff -r e13df75fee79 -r 9546828c0eb3 src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy --- 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 *)