src/HOL/Library/Formal_Power_Series.thy
changeset 36808 cbeb3484fa07
parent 36409 d323e7773aa8
child 36811 4ab4aa5bee1c
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Mon May 10 15:33:32 2010 +0200
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue May 11 08:29:42 2010 +0200
     1.3 @@ -402,7 +402,7 @@
     1.4  
     1.5  lemma number_of_fps_const: "(number_of k::('a::comm_ring_1) fps) = fps_const (of_int k)"
     1.6    
     1.7 -proof(induct k rule: int_induct[where k=0])
     1.8 +proof(induct k rule: int_bidirectional_induct [where k=0])
     1.9    case base thus ?case unfolding number_of_fps_def of_int_0 by simp
    1.10  next
    1.11    case (step1 i) thus ?case unfolding number_of_fps_def 
    1.12 @@ -3214,7 +3214,7 @@
    1.13  
    1.14  lemma fps_number_of_fps_const: "number_of i = fps_const (number_of i :: 'a:: {comm_ring_1, number_ring})"
    1.15    apply (subst (2) number_of_eq)
    1.16 -apply(rule int_induct[of _ 0])
    1.17 +apply(rule int_bidirectional_induct[of _ 0])
    1.18  apply (simp_all add: number_of_fps_def)
    1.19  by (simp_all add: fps_const_add[symmetric] fps_const_minus[symmetric])
    1.20