# HG changeset patch
# User haftmann
# Date 1503588252 -7200
# Node ID ba94aeb02fbc96139786b242b391cf5fd16fe65d
# Parent  8367a4f25781754ca2f9b2b255705efdf04ffead
more correct output syntax declaration

diff -r 8367a4f25781 -r ba94aeb02fbc src/HOL/Algebra/Multiplicative_Group.thy
--- 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 :