summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/GCD.thy

changeset 58623 | 2db1df2c8467 |

parent 57514 | bdc2c6b40bf2 |

child 58770 | ae5e9b4f8daf |

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