| changeset 60526 | fad653acf58f |
| parent 58889 | 5b7a9633cfa8 |
| child 64282 | 261d42f0bfac |
--- a/src/HOL/Number_Theory/Number_Theory.thy Fri Jun 19 21:33:03 2015 +0200 +++ b/src/HOL/Number_Theory/Number_Theory.thy Fri Jun 19 21:41:33 2015 +0200 @@ -1,5 +1,5 @@ -section {* Comprehensive number theory *} +section \<open>Comprehensive number theory\<close> theory Number_Theory imports Fib Residues Eratosthenes