src/HOL/Divides.thy
changeset 63145 703edebd1d92
parent 63040 eb4ddd18d635
child 63317 ca187a9f66da
     1.1 --- a/src/HOL/Divides.thy	Tue May 24 22:46:23 2016 +0200
     1.2 +++ b/src/HOL/Divides.thy	Wed May 25 11:49:40 2016 +0200
     1.3 @@ -1637,7 +1637,7 @@
     1.4    shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
     1.5    by (simp_all add: snd_divmod)
     1.6  
     1.7 -lemma cut_eq_simps: -- \<open>rewriting equivalence on @{text "n mod 2 ^ q"}\<close>
     1.8 +lemma cut_eq_simps: \<comment> \<open>rewriting equivalence on \<open>n mod 2 ^ q\<close>\<close>
     1.9    fixes m n q :: num
    1.10    shows
    1.11      "numeral n mod numeral Num.One = (0::nat)