doc-src/IsarRef/Thy/document/Spec.tex
changeset 30240 5b25fee0362c
parent 29706 10e6f2faa1e5
child 30242 aea5d7fa7ef5
     1.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -22,6 +22,23 @@
     1.4  }
     1.5  \isamarkuptrue%
     1.6  %
     1.7 +\begin{isamarkuptext}%
     1.8 +The Isabelle/Isar theory format integrates specifications and
     1.9 +  proofs, supporting interactive development with unlimited undo
    1.10 +  operation.  There is an integrated document preparation system (see
    1.11 +  \chref{ch:document-prep}), for typesetting formal developments
    1.12 +  together with informal text.  The resulting hyper-linked PDF
    1.13 +  documents can be used both for WWW presentation and printed copies.
    1.14 +
    1.15 +  The Isar proof language (see \chref{ch:proofs}) is embedded into the
    1.16 +  theory language as a proper sub-language.  Proof mode is entered by
    1.17 +  stating some \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory
    1.18 +  level, and left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}).  Some theory specification mechanisms also require a proof,
    1.19 +  such as \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} in HOL, which demands non-emptiness of
    1.20 +  the representing sets.%
    1.21 +\end{isamarkuptext}%
    1.22 +\isamarkuptrue%
    1.23 +%
    1.24  \isamarkupsection{Defining theories \label{sec:begin-thy}%
    1.25  }
    1.26  \isamarkuptrue%
    1.27 @@ -127,8 +144,9 @@
    1.28    \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the
    1.29    theory itself (\secref{sec:begin-thy}).
    1.30    
    1.31 -  \item \isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}{\isachardoublequote}} given after any local theory command
    1.32 -  specifies an immediate target, e.g.\ ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''.  This works both in a local or
    1.33 +  \item \isa{{\isachardoublequote}{\isacharparenleft}{\isachardoublequote}}\indexdef{}{keyword}{in}\hypertarget{keyword.in}{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}}}~\isa{{\isachardoublequote}c{\isacharparenright}{\isachardoublequote}} given after any
    1.34 +  local theory command specifies an immediate target, e.g.\
    1.35 +  ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''.  This works both in a local or
    1.36    global theory context; the current target context will be suspended
    1.37    for this command only.  Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' will
    1.38    always produce a global result independently of the current target
    1.39 @@ -792,8 +810,8 @@
    1.40    \end{matharray}
    1.41  
    1.42    \begin{mldecls}
    1.43 -    \indexml{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
    1.44 -    \indexml{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
    1.45 +    \indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
    1.46 +    \indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
    1.47    \end{mldecls}
    1.48  
    1.49    \begin{rail}
    1.50 @@ -1178,7 +1196,7 @@
    1.51  
    1.52    \end{description}
    1.53  
    1.54 -  See \hyperlink{file.~~/src/FOL/ex/IffOracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}ex{\isacharslash}IffOracle{\isachardot}thy}}}} for a worked example of
    1.55 +  See \hyperlink{file.~~/src/FOL/ex/Iff-Oracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}ex{\isacharslash}Iff{\isacharunderscore}Oracle{\isachardot}thy}}}} for a worked example of
    1.56    defining a new primitive rule as oracle, and turning it into a proof
    1.57    method.%
    1.58  \end{isamarkuptext}%