summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/GCD.thy

changeset 58623 | 2db1df2c8467 |

parent 57514 | bdc2c6b40bf2 |

child 58770 | ae5e9b4f8daf |

--- a/src/HOL/GCD.thy Tue Oct 07 23:12:08 2014 +0200 +++ b/src/HOL/GCD.thy Tue Oct 07 23:29:43 2014 +0200 @@ -8,7 +8,7 @@ This file combines and revises a number of prior developments. The original theories "GCD" and "Primes" were by Christophe Tabacznyj -and Lawrence C. Paulson, based on \cite{davenport92}. They introduced +and Lawrence C. Paulson, based on @{cite davenport92}. They introduced gcd, lcm, and prime for the natural numbers. The original theory "IntPrimes" was by Thomas M. Rasmussen, and @@ -364,7 +364,7 @@ *} lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)" - -- {* \cite[page 27]{davenport92} *} + -- {* @{cite \<open>page 27\<close> davenport92} *} apply (induct m n rule: gcd_nat_induct) apply simp apply (case_tac "k = 0")