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