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

src/HOL/Number_Theory/Primes.thy

changeset 58623 | 2db1df2c8467 |

parent 57512 | cc97b347b301 |

child 58645 | 94bef115c08f |

--- a/src/HOL/Number_Theory/Primes.thy Tue Oct 07 23:12:08 2014 +0200 +++ b/src/HOL/Number_Theory/Primes.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