--- a/src/HOL/Decision_Procs/Ferrack.thy Thu Feb 24 17:54:36 2011 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Thu Feb 24 20:52:05 2011 +0100
@@ -43,9 +43,6 @@
using Nat.gr0_conv_Suc
by clarsimp
-lemma filter_length: "length (List.filter P xs) < Suc (length xs)"
- apply (induct xs, auto) done
-
(*********************************************************************************)
(**** SHADOW SYNTAX AND SEMANTICS ****)
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Feb 24 17:54:36 2011 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Feb 24 20:52:05 2011 +0100
@@ -2472,9 +2472,6 @@
using Nat.gr0_conv_Suc
by clarsimp
-lemma filter_length: "length (List.filter P xs) < Suc (length xs)"
- apply (induct xs, auto) done
-
lemma simpfm_lin: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "qfree p \<Longrightarrow> islin (simpfm p)"
by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin)