src/HOL/Library/Periodic_Fun.thy
 changeset 62055 755fda743c49 parent 62049 b0f941e207cf child 62390 842917225d56
```     1.1 --- a/src/HOL/Library/Periodic_Fun.thy	Mon Jan 04 22:13:53 2016 +0100
1.2 +++ b/src/HOL/Library/Periodic_Fun.thy	Tue Jan 05 13:35:06 2016 +0100
1.3 @@ -1,16 +1,18 @@
1.4 -(*
1.5 -  Title:    HOL/Library/Periodic_Fun.thy
1.6 -  Author:   Manuel Eberl, TU München
1.7 -
1.8 -  A locale for periodic functions. The idea is that one proves \$f(x + p) = f(x)\$
1.9 -  for some period \$p\$ and gets derived results like \$f(x - p) = f(x)\$ and \$f(x + 2p) = f(x)\$
1.11 +(*  Title:    HOL/Library/Periodic_Fun.thy
1.12 +    Author:   Manuel Eberl, TU München
1.13  *)
1.14 +
1.15 +section \<open>Periodic Functions\<close>
1.16 +
1.17  theory Periodic_Fun
1.18  imports Complex_Main
1.19  begin
1.20
1.21  text \<open>
1.22 +  A locale for periodic functions. The idea is that one proves \$f(x + p) = f(x)\$
1.23 +  for some period \$p\$ and gets derived results like \$f(x - p) = f(x)\$ and \$f(x + 2p) = f(x)\$