src/HOL/GCD.thy
changeset 63145 703edebd1d92
parent 63025 92680537201f
child 63359 99b51ba8da1c
--- a/src/HOL/GCD.thy	Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/GCD.thy	Wed May 25 11:49:40 2016 +0200
@@ -1590,7 +1590,7 @@
 
 (* to do: add the three variations of these, and for ints? *)
 
-lemma finite_divisors_nat [simp]: -- \<open>FIXME move\<close>
+lemma finite_divisors_nat [simp]: \<comment> \<open>FIXME move\<close>
   fixes m :: nat
   assumes "m > 0" 
   shows "finite {d. d dvd m}"
@@ -1962,7 +1962,7 @@
   apply auto
   done
 
-lemma dvd_pos_nat: -- \<open>FIXME move\<close>
+lemma dvd_pos_nat: \<comment> \<open>FIXME move\<close>
   fixes n m :: nat
   assumes "n > 0" and "m dvd n"
   shows "m > 0"