changeset 63167 | 0909deb8059b |
parent 63092 | a949b2a5f51d |
child 63901 | 4ce989e962e0 |
--- a/src/HOL/Number_Theory/Cong.thy Thu May 26 16:57:14 2016 +0200 +++ b/src/HOL/Number_Theory/Cong.thy Thu May 26 17:51:22 2016 +0200 @@ -29,7 +29,7 @@ imports Primes begin -subsection \<open>Turn off @{text One_nat_def}\<close> +subsection \<open>Turn off \<open>One_nat_def\<close>\<close> lemma power_eq_one_eq_nat [simp]: "((x::nat)^m = 1) = (m = 0 | x = 1)" by (induct m) auto