src/HOL/Computational_Algebra/Squarefree.thy
changeset 67399 eab6ce8368fa
parent 67051 e7e54a0b9197
child 74543 ee039c11fb6f
--- 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 \<Longrightarrow> 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