src/HOL/Library/Periodic_Fun.thy
changeset 68406 6beb45f6cf67
parent 62390 842917225d56
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Library/Periodic_Fun.thy	Thu Jun 07 15:08:18 2018 +0200
     1.2 +++ b/src/HOL/Library/Periodic_Fun.thy	Thu Jun 07 19:36:12 2018 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4    by (subst of_nat_numeral[symmetric], subst minus_of_nat) (rule refl)
     1.5  
     1.6  lemma minus_1: "f (gn1 x) = f x"
     1.7 -  using minus_of_nat[of x 1] by (simp add: minus_1_eq minus_eq[symmetric])
     1.8 +  using minus_of_nat[of x 1] by (simp flip: minus_1_eq minus_eq)
     1.9  
    1.10  lemmas periodic_simps = plus_of_nat minus_of_nat plus_of_int minus_of_int 
    1.11                          plus_numeral minus_numeral plus_1 minus_1