src/Doc/Isar_Ref/Generic.thy
changeset 58552 66fed99e874f
parent 58310 91ea607a34d8
child 58618 782f0b662cae
     1.1 --- a/src/Doc/Isar_Ref/Generic.thy	Sun Oct 05 22:22:40 2014 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Sun Oct 05 22:24:07 2014 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4    "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the basic @{method rule}
     1.5    method (see \secref{sec:pure-meth-att}), but apply rules by
     1.6    elim-resolution, destruct-resolution, and forward-resolution,
     1.7 -  respectively \cite{isabelle-implementation}.  The optional natural
     1.8 +  respectively @{cite "isabelle-implementation"}.  The optional natural
     1.9    number argument (default 0) specifies additional assumption steps to
    1.10    be performed here.
    1.11  
    1.12 @@ -158,7 +158,7 @@
    1.13    \item @{attribute THEN}~@{text a} composes rules by resolution; it
    1.14    resolves with the first premise of @{text a} (an alternative
    1.15    position may be also specified).  See also @{ML_op "RS"} in
    1.16 -  \cite{isabelle-implementation}.
    1.17 +  @{cite "isabelle-implementation"}.
    1.18    
    1.19    \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
    1.20    folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
    1.21 @@ -319,11 +319,11 @@
    1.22  
    1.23    \item @{method rule_tac} etc. do resolution of rules with explicit
    1.24    instantiation.  This works the same way as the ML tactics @{ML
    1.25 -  res_inst_tac} etc. (see \cite{isabelle-implementation})
    1.26 +  res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
    1.27  
    1.28    Multiple rules may be only given if there is no instantiation; then
    1.29    @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
    1.30 -  \cite{isabelle-implementation}).
    1.31 +  @{cite "isabelle-implementation"}).
    1.32  
    1.33    \item @{method cut_tac} inserts facts into the proof state as
    1.34    assumption of a subgoal; instantiations may be given as well.  Note
    1.35 @@ -649,7 +649,7 @@
    1.36    @{text "(?x + ?y) + ?z \<equiv> ?x + (?y + ?z)"} \\
    1.37    @{text "f (f ?x ?y) ?z \<equiv> f ?x (f ?y ?z)"}
    1.38  
    1.39 -  \item Higher-order patterns in the sense of \cite{nipkow-patterns}.
    1.40 +  \item Higher-order patterns in the sense of @{cite "nipkow-patterns"}.
    1.41    These are terms in @{text "\<beta>"}-normal form (this will always be the
    1.42    case unless you have done something strange) where each occurrence
    1.43    of an unknown is of the form @{text "?F x\<^sub>1 \<dots> x\<^sub>n"}, where the
    1.44 @@ -846,10 +846,10 @@
    1.45  
    1.46  end
    1.47  
    1.48 -text {* Martin and Nipkow \cite{martin-nipkow} discuss the theory and
    1.49 +text {* Martin and Nipkow @{cite "martin-nipkow"} discuss the theory and
    1.50    give many examples; other algebraic structures are amenable to
    1.51    ordered rewriting, such as Boolean rings.  The Boyer-Moore theorem
    1.52 -  prover \cite{bm88book} also employs ordered rewriting.
    1.53 +  prover @{cite bm88book} also employs ordered rewriting.
    1.54  *}
    1.55  
    1.56  
    1.57 @@ -903,7 +903,7 @@
    1.58    invocation of simplification procedures.
    1.59  
    1.60    \item @{attribute simp_trace_new} controls Simplifier tracing within
    1.61 -  Isabelle/PIDE applications, notably Isabelle/jEdit \cite{isabelle-jedit}.
    1.62 +  Isabelle/PIDE applications, notably Isabelle/jEdit @{cite "isabelle-jedit"}.
    1.63    This provides a hierarchical representation of the rewriting steps
    1.64    performed by the Simplifier.
    1.65  
    1.66 @@ -1299,7 +1299,7 @@
    1.67    context.  These proof procedures are slow and simplistic compared
    1.68    with high-end automated theorem provers, but they can save
    1.69    considerable time and effort in practice.  They can prove theorems
    1.70 -  such as Pelletier's \cite{pelletier86} problems 40 and 41 in a few
    1.71 +  such as Pelletier's @{cite pelletier86} problems 40 and 41 in a few
    1.72    milliseconds (including full proof reconstruction): *}
    1.73  
    1.74  lemma "(\<exists>y. \<forall>x. F x y \<longleftrightarrow> F x x) \<longrightarrow> \<not> (\<forall>x. \<exists>y. \<forall>z. F z y \<longleftrightarrow> \<not> F z x)"
    1.75 @@ -1370,8 +1370,8 @@
    1.76    desired theorem and apply rules backwards in a fairly arbitrary
    1.77    manner.  This yields a surprisingly effective proof procedure.
    1.78    Quantifiers add only few complications, since Isabelle handles
    1.79 -  parameters and schematic variables.  See \cite[Chapter
    1.80 -  10]{paulson-ml2} for further discussion.  *}
    1.81 +  parameters and schematic variables.  See @{cite \<open>Chapter 10\<close>
    1.82 +  "paulson-ml2"} for further discussion.  *}
    1.83  
    1.84  
    1.85  subsubsection {* Simulating sequents by natural deduction *}