diff -r 0a2a1b6507c1 -r 493b818e8e10 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Wed Apr 18 21:12:50 2018 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Wed May 02 13:49:38 2018 +0200
@@ -105,9 +105,6 @@
 lemma cond_value_iff: "f (if b then x else y) = (if b then f x else f y)"
   by auto
 
-lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
-  by auto
-
 
 subsection \<open>Formal power series form a commutative ring with unity, if the range of sequences
   they represent is a commutative ring with unity\<close>