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