# HG changeset patch # User wenzelm # Date 1412542027 -7200 # Node ID 7975676c08c0eb3ff3b94375430843f18b15f6e1 # Parent 423202f05a431e3fa30bda68849d9939074c8bec prefer @{cite} antiquotation; diff -r 423202f05a43 -r 7975676c08c0 src/Doc/Implementation/Eq.thy --- a/src/Doc/Implementation/Eq.thy Sun Oct 05 22:46:20 2014 +0200 +++ b/src/Doc/Implementation/Eq.thy Sun Oct 05 22:47:07 2014 +0200 @@ -76,7 +76,7 @@ %FIXME The classic article that introduces the concept of conversion (for - Cambridge LCF) is \cite{paulson:1983}. + Cambridge LCF) is @{cite "paulson:1983"}. *} diff -r 423202f05a43 -r 7975676c08c0 src/Doc/Implementation/Integration.thy --- a/src/Doc/Implementation/Integration.thy Sun Oct 05 22:46:20 2014 +0200 +++ b/src/Doc/Implementation/Integration.thy Sun Oct 05 22:47:07 2014 +0200 @@ -15,7 +15,8 @@ stateless manner. Historically, the sequence of transitions was wrapped up as sequential command loop, such that commands are applied one-by-one. In contemporary Isabelle/Isar, processing toplevel commands usually works in - parallel in multi-threaded Isabelle/ML \cite{Wenzel:2009,Wenzel:2013:ITP}. + parallel in multi-threaded Isabelle/ML @{cite "Wenzel:2009" and + "Wenzel:2013:ITP"}. *} @@ -182,7 +183,7 @@ sub-graph of theories, the intrinsic parallelism can be exploited by the system to speedup loading. - This variant is used by default in @{tool build} \cite{isabelle-sys}. + This variant is used by default in @{tool build} @{cite "isabelle-sys"}. \item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value presently associated with name @{text A}. Note that the result might be diff -r 423202f05a43 -r 7975676c08c0 src/Doc/Implementation/Isar.thy --- a/src/Doc/Implementation/Isar.thy Sun Oct 05 22:46:20 2014 +0200 +++ b/src/Doc/Implementation/Isar.thy Sun Oct 05 22:47:07 2014 +0200 @@ -5,7 +5,7 @@ chapter {* Isar language elements *} text {* The Isar proof language (see also - \cite[\S2]{isabelle-isar-ref}) consists of three main categories of + @{cite \\S2\ "isabelle-isar-ref"}) consists of three main categories of language elements: \begin{enumerate} @@ -96,7 +96,7 @@ unless a certain linguistic mode is active, namely ``@{text "proof(state)"}'', ``@{text "proof(chain)"}'', ``@{text "proof(prove)"}'', respectively (using the terminology of - \cite{isabelle-isar-ref}). + @{cite "isabelle-isar-ref"}). It is advisable study the implementations of existing proof commands for suitable modes to be asserted. @@ -351,7 +351,7 @@ *} text %mlex {* See also @{command method_setup} in - \cite{isabelle-isar-ref} which includes some abstract examples. + @{cite "isabelle-isar-ref"} which includes some abstract examples. \medskip The following toy examples illustrate how the goal facts and state are passed to proof methods. The predefined proof method @@ -394,7 +394,7 @@ The @{ML Attrib.thms} parser produces a list of theorems from the usual Isar syntax involving attribute expressions etc.\ (syntax - category @{syntax thmrefs}) \cite{isabelle-isar-ref}. The resulting + category @{syntax thmrefs}) @{cite "isabelle-isar-ref"}. The resulting @{ML_text thms} are added to @{ML HOL_basic_ss} which already contains the basic Simplifier setup for HOL. @@ -575,6 +575,6 @@ *} text %mlex {* See also @{command attribute_setup} in - \cite{isabelle-isar-ref} which includes some abstract examples. *} + @{cite "isabelle-isar-ref"} which includes some abstract examples. *} end diff -r 423202f05a43 -r 7975676c08c0 src/Doc/Implementation/Local_Theory.thy --- a/src/Doc/Implementation/Local_Theory.thy Sun Oct 05 22:46:20 2014 +0200 +++ b/src/Doc/Implementation/Local_Theory.thy Sun Oct 05 22:47:07 2014 +0200 @@ -90,7 +90,7 @@ reset to the target context. The target now holds definitions for terms and theorems that stem from the hypothetical @{text "\"} and @{text "\"} elements, transformed by the - particular target policy (see \cite[\S4--5]{Haftmann-Wenzel:2009} + particular target policy (see @{cite \\S4--5\ "Haftmann-Wenzel:2009"} for details). *} text %mlref {* @@ -159,7 +159,7 @@ text {* %FIXME - See also \cite{Chaieb-Wenzel:2007}. + See also @{cite "Chaieb-Wenzel:2007"}. *} end diff -r 423202f05a43 -r 7975676c08c0 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Sun Oct 05 22:46:20 2014 +0200 +++ b/src/Doc/Implementation/Logic.thy Sun Oct 05 22:47:07 2014 +0200 @@ -7,9 +7,9 @@ text {* The logical foundations of Isabelle/Isar are that of the Pure logic, which has been introduced as a Natural Deduction framework in - \cite{paulson700}. This is essentially the same logic as ``@{text + @{cite paulson700}. This is essentially the same logic as ``@{text "\HOL"}'' in the more abstract setting of Pure Type Systems (PTS) - \cite{Barendregt-Geuvers:2001}, although there are some key + @{cite "Barendregt-Geuvers:2001"}, although there are some key differences in the specific treatment of simple types in Isabelle/Pure. @@ -112,7 +112,7 @@ \\<^bsub>s\<^sub>k\<^esub>)\"} is of sort @{text "s"}. Consequently, type unification has most general solutions (modulo equivalence of sorts), so type-inference produces primary types as - expected \cite{nipkow-prehofer}. + expected @{cite "nipkow-prehofer"}. *} text %mlref {* @@ -237,8 +237,8 @@ text {* The language of terms is that of simply-typed @{text "\"}-calculus - with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72} - or \cite{paulson-ml2}), with the types being determined by the + with de-Bruijn indices for bound variables (cf.\ @{cite debruijn72} + or @{cite "paulson-ml2"}), with the types being determined by the corresponding binders. In contrast, free variables and constants have an explicit name and type in each occurrence. @@ -558,7 +558,7 @@ explicit proof terms for primitive inferences, see also \secref{sec:proof-terms}. Thus all three levels of @{text "\"}-calculus become explicit: @{text "\"} for terms, and @{text - "\/\"} for proofs (cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}). + "\/\"} for proofs (cf.\ @{cite "Berghofer-Nipkow:2000:TPHOL"}). Observe that locally fixed parameters (as in @{text "\\intro"}) need not be recorded in the hypotheses, because @@ -566,7 +566,7 @@ ``Assumptions'' @{text "x :: \"} for type-membership are only present as long as some @{text "x\<^sub>\"} occurs in the statement body.\footnote{This is the key difference to ``@{text "\HOL"}'' in - the PTS framework \cite{Barendregt-Geuvers:2001}, where hypotheses + the PTS framework @{cite "Barendregt-Geuvers:2001"}, where hypotheses @{text "x : A"} are treated uniformly for propositions and types.} \medskip The axiomatization of a theory is implicitly closed by @@ -628,7 +628,7 @@ "d(\\<^sub>i)"} for some @{text "\\<^sub>i"} projected from @{text "\<^vec>\"}. Thus overloaded definitions essentially work by primitive recursion over the syntactic structure of a single type - argument. See also \cite[\S4.3]{Haftmann-Wenzel:2006:classes}. + argument. See also @{cite \\S4.3\ "Haftmann-Wenzel:2006:classes"}. *} text %mlref {* @@ -1009,8 +1009,8 @@ text {* The idea of object-level rules is to model Natural Deduction - inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow - arbitrary nesting similar to \cite{extensions91}. The most basic + inferences in the style of Gentzen @{cite "Gentzen:1935"}, but we allow + arbitrary nesting similar to @{cite extensions91}. The most basic rule format is that of a \emph{Horn Clause}: \[ \infer{@{text "A"}}{@{text "A\<^sub>1"} & @{text "\"} & @{text "A\<^sub>n"}} @@ -1033,7 +1033,7 @@ Nesting of rules means that the positions of @{text "A\<^sub>i"} may again hold compound rules, not just atomic propositions. Propositions of this format are called \emph{Hereditary Harrop - Formulae} in the literature \cite{Miller:1991}. Here we give an + Formulae} in the literature @{cite "Miller:1991"}. Here we give an inductive characterization as follows: \medskip @@ -1222,7 +1222,7 @@ according to the propositions-as-types principle. The resulting 3-level @{text "\"}-calculus resembles ``@{text "\HOL"}'' in the more abstract setting of Pure Type Systems (PTS) - \cite{Barendregt-Geuvers:2001}, if some fine points like schematic + @{cite "Barendregt-Geuvers:2001"}, if some fine points like schematic polymorphism and type classes are ignored. \medskip\emph{Proof abstractions} of the form @{text "\<^bold>\x :: \. prf"} @@ -1284,7 +1284,7 @@ There are separate operations to reconstruct the full proof term later on, using \emph{higher-order pattern unification} - \cite{nipkow-patterns,Berghofer-Nipkow:2000:TPHOL}. + @{cite "nipkow-patterns" and "Berghofer-Nipkow:2000:TPHOL"}. The \emph{proof checker} expects a fully reconstructed proof term, and can turn it into a theorem by replaying its primitive inferences @@ -1294,7 +1294,7 @@ subsection {* Concrete syntax of proof terms *} text {* The concrete syntax of proof terms is a slight extension of - the regular inner syntax of Isabelle/Pure \cite{isabelle-isar-ref}. + the regular inner syntax of Isabelle/Pure @{cite "isabelle-isar-ref"}. Its main syntactic category @{syntax (inner) proof} is defined as follows: diff -r 423202f05a43 -r 7975676c08c0 src/Doc/Implementation/ML.thy --- a/src/Doc/Implementation/ML.thy Sun Oct 05 22:46:20 2014 +0200 +++ b/src/Doc/Implementation/ML.thy Sun Oct 05 22:47:07 2014 +0200 @@ -681,7 +681,7 @@ \} Here @{syntax nameref} and @{syntax args} are outer syntax categories, as - defined in \cite{isabelle-isar-ref}. + defined in @{cite "isabelle-isar-ref"}. \medskip A regular antiquotation @{text "@{name args}"} processes its arguments by the usual means of the Isar source language, and @@ -1008,7 +1008,7 @@ batch sessions prefixes each line of warnings by @{verbatim "###"} and errors by @{verbatim "***"}, but leaves anything else unchanged. The message body may contain further markup and formatting, - which is routinely used in the Prover IDE \cite{isabelle-jedit}. + which is routinely used in the Prover IDE @{cite "isabelle-jedit"}. Messages are associated with the transaction context of the running Isar command. This enables the front-end to manage commands and @@ -1325,7 +1325,7 @@ \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify standard symbols according to fixed syntactic conventions of Isabelle, cf.\ - \cite{isabelle-isar-ref}. + @{cite "isabelle-isar-ref"}. \item Type @{ML_type "Symbol.sym"} is a concrete datatype that represents the different kinds of symbols explicitly, with @@ -1404,7 +1404,7 @@ \item sequence of Isabelle symbols (see also \secref{sec:symbols}), with @{ML Symbol.explode} as key operation; - \item XML tree structure via YXML (see also \cite{isabelle-sys}), + \item XML tree structure via YXML (see also @{cite "isabelle-sys"}), with @{ML YXML.parse_body} as key operation. \end{enumerate} @@ -1686,15 +1686,15 @@ Law'' follows different rules: clock frequency has reached its peak around 2005, and applications need to be parallelized in order to avoid a perceived loss of performance. See also - \cite{Sutter:2005}.} + @{cite "Sutter:2005"}.} Isabelle/Isar exploits the inherent structure of theories and proofs to support \emph{implicit parallelism} to a large extent. LCF-style theorem proving provides almost ideal conditions for that, see also - \cite{Wenzel:2009}. This means, significant parts of theory and proof + @{cite "Wenzel:2009"}. This means, significant parts of theory and proof checking is parallelized by default. In Isabelle2013, a maximum speedup-factor of 3.5 on 4 cores and 6.5 on 8 cores can be expected - \cite{Wenzel:2013:ITP}. + @{cite "Wenzel:2013:ITP"}. \medskip ML threads lack the memory protection of separate processes, and operate concurrently on shared heap memory. This has @@ -2156,11 +2156,11 @@ text {* Futures help to organize parallel execution in a value-oriented manner, with @{text fork}~/ @{text join} as the main pair of operations, and some further - variants; see also \cite{Wenzel:2009,Wenzel:2013:ITP}. Unlike lazy values, - futures are evaluated strictly and spontaneously on separate worker threads. - Futures may be canceled, which leads to interrupts on running evaluation - attempts, and forces structurally related futures to fail for all time; - already finished futures remain unchanged. Exceptions between related + variants; see also @{cite "Wenzel:2009" and "Wenzel:2013:ITP"}. Unlike lazy + values, futures are evaluated strictly and spontaneously on separate worker + threads. Futures may be canceled, which leads to interrupts on running + evaluation attempts, and forces structurally related futures to fail for all + time; already finished futures remain unchanged. Exceptions between related futures are propagated as well, and turned into parallel exceptions (see above). diff -r 423202f05a43 -r 7975676c08c0 src/Doc/Implementation/Prelim.thy --- a/src/Doc/Implementation/Prelim.thy Sun Oct 05 22:46:20 2014 +0200 +++ b/src/Doc/Implementation/Prelim.thy Sun Oct 05 22:47:07 2014 +0200 @@ -58,7 +58,7 @@ elimination rules for arbitrary operators (depending on the object-logic and application), which enables users to perform standard proof steps implicitly (cf.\ the @{text "rule"} method - \cite{isabelle-isar-ref}). + @{cite "isabelle-isar-ref"}). \medskip Thus Isabelle/Isar is able to bring forth more and more concepts successively. In particular, an object-logic like diff -r 423202f05a43 -r 7975676c08c0 src/Doc/Implementation/Proof.thy --- a/src/Doc/Implementation/Proof.thy Sun Oct 05 22:46:20 2014 +0200 +++ b/src/Doc/Implementation/Proof.thy Sun Oct 05 22:47:07 2014 +0200 @@ -380,7 +380,7 @@ conclusion: the proof demonstrates that the context may be augmented by parameters and assumptions, without affecting any conclusions that do not mention these parameters. See also - \cite{isabelle-isar-ref} for the user-level @{command obtain} and + @{cite "isabelle-isar-ref"} for the user-level @{command obtain} and @{command guess} elements. Final results, which may not refer to the parameters in the conclusion, need to exported explicitly into the original context. *} diff -r 423202f05a43 -r 7975676c08c0 src/Doc/Implementation/Syntax.thy --- a/src/Doc/Implementation/Syntax.thy Sun Oct 05 22:46:20 2014 +0200 +++ b/src/Doc/Implementation/Syntax.thy Sun Oct 05 22:47:07 2014 +0200 @@ -12,13 +12,13 @@ additional means for reading and printing of terms and types. This important add-on outside the logical core is called \emph{inner syntax} in Isabelle jargon, as opposed to the \emph{outer syntax} of - the theory and proof language \cite{isabelle-isar-ref}. + the theory and proof language @{cite "isabelle-isar-ref"}. - For example, according to \cite{church40} quantifiers are represented as + For example, according to @{cite church40} quantifiers are represented as higher-order constants @{text "All :: ('a \ bool) \ bool"} such that @{text "All (\x::'a. B x)"} faithfully represents the idea that is displayed in Isabelle as @{text "\x::'a. B x"} via @{keyword "binder"} notation. - Moreover, type-inference in the style of Hindley-Milner \cite{hindleymilner} + Moreover, type-inference in the style of Hindley-Milner @{cite hindleymilner} (and extensions) enables users to write @{text "\x. B x"} concisely, when the type @{text "'a"} is already clear from the context.\footnote{Type-inference taken to the extreme can easily confuse @@ -133,9 +133,9 @@ \medskip Note that the string values that are passed in and out are annotated by the system, to carry further markup that is relevant for the - Prover IDE \cite{isabelle-jedit}. User code should neither compose its own - input strings, nor try to analyze the output strings. Conceptually this is - an abstract datatype, encoded as concrete string for historical reasons. + Prover IDE @{cite "isabelle-jedit"}. User code should neither compose its + own input strings, nor try to analyze the output strings. Conceptually this + is an abstract datatype, encoded as concrete string for historical reasons. The standard way to provide the required position markup for input works via the outer syntax parser wrapper @{ML Parse.inner_syntax}, which is already @@ -161,9 +161,10 @@ declaratively via mixfix annotations. Moreover, there are \emph{syntax translations} that can be augmented by the user, either declaratively via @{command translations} or programmatically via @{command - parse_translation}, @{command print_translation} \cite{isabelle-isar-ref}. - The final scope-resolution is performed by the system, according to name - spaces for types, term variables and constants determined by the context. + parse_translation}, @{command print_translation} @{cite + "isabelle-isar-ref"}. The final scope-resolution is performed by the system, + according to name spaces for types, term variables and constants determined + by the context. *} text %mlref {* @@ -216,7 +217,7 @@ before pretty printing. A typical add-on for the check/uncheck syntax layer is the @{command - abbreviation} mechanism \cite{isabelle-isar-ref}. Here the user specifies + abbreviation} mechanism @{cite "isabelle-isar-ref"}. Here the user specifies syntactic definitions that are managed by the system as polymorphic @{text "let"} bindings. These are expanded during the @{text "check"} phase, and contracted during the @{text "uncheck"} phase, without affecting the @@ -230,7 +231,7 @@ constants according to the ``dictionary construction'' of its logical foundation. This involves ``type improvement'' (specialization of slightly too general types) and replacement by - certain locale parameters. See also \cite{Haftmann-Wenzel:2009}. + certain locale parameters. See also @{cite "Haftmann-Wenzel:2009"}. *} text %mlref {*