# HG changeset patch
# User krauss
# Date 1298577125 -3600
# Node ID c845adaecf988d40f6a47aef84053ac14490ef23
# Parent  6fc224dc54731f1bd9e9949c49c01e01013217c2
removed unused lemma

diff -r 6fc224dc5473 -r c845adaecf98 src/HOL/Decision_Procs/Ferrack.thy
--- 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                  ****)
diff -r 6fc224dc5473 -r c845adaecf98 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- 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)