src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 41838 c845adaecf98
parent 41823 81d64ec48427
child 41842 d8f76db6a207
--- 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)