diff -r 5eb932e604a2 -r eab6ce8368fa src/HOL/Computational_Algebra/Squarefree.thy --- a/src/HOL/Computational_Algebra/Squarefree.thy Wed Jan 10 15:21:49 2018 +0100 +++ b/src/HOL/Computational_Algebra/Squarefree.thy Wed Jan 10 15:25:09 2018 +0100 @@ -360,4 +360,4 @@ "odd n \ square_part (x ^ n) = normalize (x ^ (n div 2) * square_part x)" by (subst square_part_odd_power' [symmetric]) auto -end \ No newline at end of file +end