src/HOL/Old_Number_Theory/Legacy_GCD.thy

 \<close>
 
 subsection \<open>Specification of GCD on nats\<close>
 
 definition
-  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- \<open>@{term gcd} as a relation\<close>
+  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where \<comment> \<open>@{term gcd} as a relation\<close>
   "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
     (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
 
 text \<open>Uniqueness\<close>
 

   unfolding One_nat_def by (rule gcd_1)
 
 declare gcd.simps [simp del]
 
 text \<open>
-  \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
+  \medskip @{term "gcd m n"} divides \<open>m\<close> and \<open>n\<close>.  The
   conjunctions don't seem provable separately.
 \<close>
 
 lemma gcd_dvd1 [iff, algebra]: "gcd m n dvd m"
   and gcd_dvd2 [iff, algebra]: "gcd m n dvd n"

 text \<open>
   \medskip Multiplication laws
 \<close>
 
 lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)"
-    -- \<open>@{cite \<open>page 27\<close> davenport92}\<close>
+    \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
   apply (induct m n rule: gcd_induct)
    apply simp
   apply (case_tac "k = 0")
    apply (simp_all add: gcd_non_0)
   done

   apply (rule zgcd_assoc [THEN trans])
   apply (rule zgcd_commute [THEN arg_cong])
   done
 
 lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
-  -- \<open>addition is an AC-operator\<close>
+  \<comment> \<open>addition is an AC-operator\<close>
 
 lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
   by (simp del: minus_mult_right [symmetric]
       add: minus_mult_right nat_mult_distrib zgcd_def abs_if
           mult_less_0_iff gcd_mult_distrib2 [symmetric] of_nat_mult)