author | haftmann |
Thu, 24 Aug 2017 17:24:12 +0200 | |
changeset 66500 | ba94aeb02fbc |
parent 66499 | 8367a4f25781 |
child 66501 | 5a42eddc11c1 |
--- a/src/HOL/Algebra/Multiplicative_Group.thy Thu Aug 24 21:56:26 2017 +0200 +++ b/src/HOL/Algebra/Multiplicative_Group.thy Thu Aug 24 17:24:12 2017 +0200 @@ -141,7 +141,7 @@ definition phi' :: "nat => nat" where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}" -notation (latex_output) +notation (latex output) phi' ("\<phi> _") lemma phi'_nonzero :