changeset 61382 | efac889fccbc |
parent 58889 | 5b7a9633cfa8 |
child 62481 | b5d8e57826df |
--- a/src/HOL/Old_Number_Theory/Pocklington.thy Sat Oct 10 16:21:34 2015 +0200 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy Sat Oct 10 16:26:23 2015 +0200 @@ -2,7 +2,7 @@ Author: Amine Chaieb *) -section {* Pocklington's Theorem for Primes *} +section \<open>Pocklington's Theorem for Primes\<close> theory Pocklington imports Primes