src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 41838 c845adaecf98
parent 41823 81d64ec48427
child 41842 d8f76db6a207
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Feb 24 17:54:36 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Feb 24 20:52:05 2011 +0100
     1.3 @@ -2472,9 +2472,6 @@
     1.4  using Nat.gr0_conv_Suc
     1.5  by clarsimp
     1.6  
     1.7 -lemma filter_length: "length (List.filter P xs) < Suc (length xs)"
     1.8 -  apply (induct xs, auto) done
     1.9 -
    1.10  lemma simpfm_lin:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    1.11    shows "qfree p \<Longrightarrow> islin (simpfm p)"
    1.12    by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin)