removed unused lemma
authorkrauss
Thu Feb 24 20:52:05 2011 +0100 (2011-02-24)
changeset 41838c845adaecf98
parent 41837 6fc224dc5473
child 41839 421a795cee05
removed unused lemma
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
     1.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Feb 24 17:54:36 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Feb 24 20:52:05 2011 +0100
     1.3 @@ -43,9 +43,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  
    1.11    (*********************************************************************************)
    1.12    (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
     2.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Feb 24 17:54:36 2011 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Feb 24 20:52:05 2011 +0100
     2.3 @@ -2472,9 +2472,6 @@
     2.4  using Nat.gr0_conv_Suc
     2.5  by clarsimp
     2.6  
     2.7 -lemma filter_length: "length (List.filter P xs) < Suc (length xs)"
     2.8 -  apply (induct xs, auto) done
     2.9 -
    2.10  lemma simpfm_lin:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    2.11    shows "qfree p \<Longrightarrow> islin (simpfm p)"
    2.12    by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin)