--- a/src/Doc/Codegen/Computations.thy Fri Dec 29 18:09:38 2017 +0100
+++ b/src/Doc/Codegen/Computations.thy Fri Dec 29 19:17:52 2017 +0100
@@ -263,7 +263,7 @@
text \<open>
Computations are a device to implement fast proof procedures.
Then results of a computation are often assumed to be trustable
- and thus wrapped in oracles (see \cite{isabelle-isar-ref}),
+ and thus wrapped in oracles (see @{cite "isabelle-isar-ref"}),
as in the following example:\footnote{
The technical details how numerals are dealt with are given later in
\secref{sec:literal_input}.}
@@ -294,7 +294,7 @@
text \<open>
\<^item> Antiquotation @{ML_antiquotation computation_conv} basically yields
a conversion of type @{ML_type "Proof.context -> cterm -> thm"}
- (see further \cite{isabelle-implementation}).
+ (see further @{cite "isabelle-implementation"}).
\<^item> The antiquotation expects one functional argument to bridge the
\qt{untrusted gap}; this can be done e.g.~using an oracle. Since that oracle
--- a/src/Doc/Prog_Prove/Isar.thy Fri Dec 29 18:09:38 2017 +0100
+++ b/src/Doc/Prog_Prove/Isar.thy Fri Dec 29 19:17:52 2017 +0100
@@ -505,7 +505,7 @@
Therefore the \isakeyword{also} hidden in \isakeyword{finally} sets \<open>calculation\<close>
to \<open>t\<^sub>1 < t\<^sub>4\<close> and the final ``\texttt{.}'' succeeds.
-For more information on this style of proof see \cite{BauerW-TPHOLs01}.
+For more information on this style of proof see @{cite "BauerW-TPHOLs01"}.
\fi
\section{Streamlining Proofs}
--- a/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy Fri Dec 29 18:09:38 2017 +0100
+++ b/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy Fri Dec 29 19:17:52 2017 +0100
@@ -28,8 +28,8 @@
instantiating type-classes, adding relationships between
locales (@{command sublocale}) and type-classes
(@{command subclass}). Handy introductions are the
- respective tutorials \cite{isabelle-locale}
- \cite{isabelle-classes}.
+ respective tutorials @{cite "isabelle-locale"}
+ @{cite "isabelle-classes"}.
\<close>
subsection \<open>Strengths and restrictions of type classes\<close>
@@ -48,7 +48,7 @@
to the numerical type on the right hand side.
How to accomplish this given the quite restrictive type system
- of {Isabelle/HOL}? Paulson \cite{paulson-numerical} explains
+ of {Isabelle/HOL}? Paulson @{cite "paulson-numerical"} explains
that each numerical type has some characteristic properties
which define an characteristic algebraic structure; @{text \<sqsubset>}
then corresponds to specialization of the corresponding
@@ -122,7 +122,7 @@
optionally showing the logical content for each class also.
Optional parameters restrict the graph to a particular segment
which is useful to get a graspable view. See
- the Isar reference manual \cite{isabelle-isar-ref} for details.
+ the Isar reference manual @{cite "isabelle-isar-ref"} for details.
\<close>
@@ -144,7 +144,7 @@
\<^item> @{command class} @{class one} with @{term [source] "1::'a::one"}
\noindent Before the introduction of the @{command class} statement in
- Isabelle \cite{Haftmann-Wenzel:2006:classes} it was impossible
+ Isabelle @{cite "Haftmann-Wenzel:2006:classes"} it was impossible
to define operations with associated axioms in the same class,
hence there were always pairs of syntactic and logical type
classes. This restriction is lifted nowadays, but there are
--- a/src/HOL/Algebra/Multiplicative_Group.thy Fri Dec 29 18:09:38 2017 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy Fri Dec 29 19:17:52 2017 +0100
@@ -724,7 +724,7 @@
text \<open>
In this section we show that the multiplicative group of a finite field
is generated by a single element, i.e. it is cyclic. The proof is inspired
- by the first proof given in the survey~\cite{conrad-cyclicity}.
+ by the first proof given in the survey~@{cite "conrad-cyclicity"}.
\<close>
lemma (in group) pow_order_eq_1:
--- a/src/HOL/Algebra/document/root.bib Fri Dec 29 18:09:38 2017 +0100
+++ b/src/HOL/Algebra/document/root.bib Fri Dec 29 19:17:52 2017 +0100
@@ -7,6 +7,13 @@
note = {Also Computer Laboratory Technical Report number 473.}
}
+@Misc{conrad-cyclicity,
+ author = {Keith Conrad},
+ title = {CYCLICITY OF {$(Z/(p))^x$}},
+ howpublished = {Expository paper from the author's website},
+ note = {\url{http://www.math.uconn.edu/~kconrad/blurbs/grouptheory/cyclicFp.pdf}},
+}
+
@Book{Jacobson:1985,
author = {Nathan Jacobson},
title = {Basic Algebra I},
@@ -20,6 +27,6 @@
Abstract Algebra with {Isabelle HOL}},
journal = {J. Automated Reasoning},
year = 1999,
- number = 23,
+ volume = 23,
pages = {235--264}
}
--- a/src/HOL/Binomial.thy Fri Dec 29 18:09:38 2017 +0100
+++ b/src/HOL/Binomial.thy Fri Dec 29 19:17:52 2017 +0100
@@ -708,7 +708,7 @@
using binomial_symmetric[of k n] by (simp add: binomial_gbinomial [symmetric])
-text \<open>The absorption identity (equation 5.5 \cite[p.~157]{GKP}):
+text \<open>The absorption identity (equation 5.5 @{cite \<open>p.~157\<close> GKP_CM}):
\[
{r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0.
\]\<close>
@@ -718,7 +718,7 @@
text \<open>The absorption identity is written in the following form to avoid
division by $k$ (the lower index) and therefore remove the $k \neq 0$
-restriction\cite[p.~157]{GKP}:
+restriction @{cite \<open>p.~157\<close> GKP_CM}:
\[
k{r \choose k} = r{r - 1 \choose k - 1}, \quad \textnormal{integer } k.
\]\<close>
@@ -730,7 +730,7 @@
by (cases n) (simp_all add: binomial_eq_0 Suc_times_binomial del: binomial_Suc_Suc mult_Suc)
text \<open>The absorption companion identity for natural number coefficients,
- following the proof by GKP \cite[p.~157]{GKP}:\<close>
+ following the proof by GKP @{cite \<open>p.~157\<close> GKP_CM}:\<close>
lemma binomial_absorb_comp: "(n - k) * (n choose k) = n * ((n - 1) choose k)"
(is "?lhs = ?rhs")
proof (cases "n \<le> k")
@@ -761,7 +761,7 @@
by (subst choose_reduce_nat) simp_all
text \<open>
- Equation 5.9 of the reference material \cite[p.~159]{GKP} is a useful
+ Equation 5.9 of the reference material @{cite \<open>p.~159\<close> GKP_CM} is a useful
summation formula, operating on both indices:
\[
\sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n},
@@ -783,7 +783,7 @@
subsubsection \<open>Summation on the upper index\<close>
text \<open>
- Another summation formula is equation 5.10 of the reference material \cite[p.~160]{GKP},
+ Another summation formula is equation 5.10 of the reference material @{cite \<open>p.~160\<close> GKP_CM},
aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} =
{n + 1 \choose m + 1}, \quad \textnormal{integers } m, n \geq 0.\]
\<close>
--- a/src/HOL/HOL.thy Fri Dec 29 18:09:38 2017 +0100
+++ b/src/HOL/HOL.thy Fri Dec 29 19:17:52 2017 +0100
@@ -56,7 +56,7 @@
subsection \<open>Primitive logic\<close>
text \<open>
-The definition of the logic is based on Mike Gordon's technical report \cite{Gordon-TR68} that
+The definition of the logic is based on Mike Gordon's technical report @{cite "Gordon-TR68"} that
describes the first implementation of HOL. However, there are a number of differences.
In particular, we start with the definite description operator and introduce Hilbert's \<open>\<epsilon>\<close> operator
only much later. Moreover, axiom \<open>(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)\<close> is derived from the other
--- a/src/HOL/document/root.bib Fri Dec 29 18:09:38 2017 +0100
+++ b/src/HOL/document/root.bib Fri Dec 29 19:17:52 2017 +0100
@@ -12,6 +12,16 @@
year = 1992
}
+@book{GKP_CM,
+ author = {Graham, Ronald L. and Knuth, Donald E. and Patashnik, Oren},
+ title = {Concrete Mathematics: A Foundation for Computer Science},
+ year = {1994},
+ isbn = {0201558025},
+ edition = {2nd},
+ publisher = {Addison--Wesley},
+ address = {Boston, MA, USA},
+}
+
@techreport{Gordon-TR68,
author = "Mike Gordon",
title = "{HOL}: {A} Machine Oriented Formulation of Higher-Order Logic",