src/HOL/Library/Periodic_Fun.thy
changeset 62390 842917225d56
parent 62055 755fda743c49
child 68406 6beb45f6cf67
     1.1 --- a/src/HOL/Library/Periodic_Fun.thy	Tue Feb 23 15:37:18 2016 +0100
     1.2 +++ b/src/HOL/Library/Periodic_Fun.thy	Tue Feb 23 16:25:08 2016 +0100
     1.3 @@ -129,4 +129,4 @@
     1.4  interpretation cot: periodic_fun_simple cot "2 * of_real pi :: 'a :: {real_normed_field,banach}"
     1.5    by standard (simp only: cot_def [abs_def] sin.plus_1 cos.plus_1)
     1.6    
     1.7 -end
     1.8 \ No newline at end of file
     1.9 +end