| changeset 61933 | cf58b5b794b2 |
| parent 61762 | d50b993b4fb9 |
| child 63534 | 523b488b15c9 |
--- a/src/HOL/ex/Sqrt_Script.thy Sat Dec 26 15:44:14 2015 +0100 +++ b/src/HOL/ex/Sqrt_Script.thy Sat Dec 26 15:59:27 2015 +0100 @@ -52,7 +52,7 @@ subsection \<open>Main theorem\<close> text \<open> - The square root of any prime number (including @{text 2}) is + The square root of any prime number (including \<open>2\<close>) is irrational. \<close>