doc-src/IsarRef/Thy/document/Introduction.tex

added warning about inconsistent context to Metis;
it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent

%
\begin{isabellebody}%
\def\isabellecontext{Introduction}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Introduction\isanewline
\isakeyword{imports}\ Main\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Introduction%
}
\isamarkuptrue%
%
\isamarkupsection{Overview%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \emph{Isabelle} system essentially provides a generic
  infrastructure for building deductive systems (programmed in
  Standard ML), with a special focus on interactive theorem proving in
  higher-order logics.  Many years ago, even end-users would refer to
  certain ML functions (goal commands, tactics, tacticals etc.) to
  pursue their everyday theorem proving tasks.
  
  In contrast \emph{Isar} provides an interpreted language environment
  of its own, which has been specifically tailored for the needs of
  theory and proof development.  Compared to raw ML, the Isabelle/Isar
  top-level provides a more robust and comfortable development
  platform, with proper support for theory development graphs, managed
  transactions with unlimited undo etc.  The Isabelle/Isar version of
  the \emph{Proof~General} user interface
  \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end
  for interactive theory and proof development in this advanced
  theorem proving environment, even though it is somewhat biased
  towards old-style proof scripts.

  \medskip Apart from the technical advances over bare-bones ML
  programming, the main purpose of the Isar language is to provide a
  conceptually different view on machine-checked proofs
  \cite{Wenzel:1999:TPHOL,Wenzel-PhD}.  \emph{Isar} stands for
  \emph{Intelligible semi-automated reasoning}.  Drawing from both the
  traditions of informal mathematical proof texts and high-level
  programming languages, Isar offers a versatile environment for
  structured formal proof documents.  Thus properly written Isar
  proofs become accessible to a broader audience than unstructured
  tactic scripts (which typically only provide operational information
  for the machine).  Writing human-readable proof texts certainly
  requires some additional efforts by the writer to achieve a good
  presentation, both of formal and informal parts of the text.  On the
  other hand, human-readable formal texts gain some value in their own
  right, independently of the mechanic proof-checking process.

  Despite its grand design of structured proof texts, Isar is able to
  assimilate the old tactical style as an ``improper'' sub-language.
  This provides an easy upgrade path for existing tactic scripts, as
  well as some means for interactive experimentation and debugging of
  structured proofs.  Isabelle/Isar supports a broad range of proof
  styles, both readable and unreadable ones.

  \medskip The generic Isabelle/Isar framework (see
  \chref{ch:isar-framework}) works reasonably well for any Isabelle
  object-logic that conforms to the natural deduction view of the
  Isabelle/Pure framework.  Specific language elements introduced by
  the major object-logics are described in \chref{ch:hol}
  (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
  (Isabelle/ZF).  The main language elements are already provided by
  the Isabelle/Pure framework. Nevertheless, examples given in the
  generic parts will usually refer to Isabelle/HOL as well.

  \medskip Isar commands may be either \emph{proper} document
  constructors, or \emph{improper commands}.  Some proof methods and
  attributes introduced later are classified as improper as well.
  Improper Isar language elements, which are marked by ``\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}'' in the subsequent chapters; they are often helpful
  when developing proof documents, but their use is discouraged for
  the final human-readable outcome.  Typical examples are diagnostic
  commands that print terms or theorems according to the current
  context; other commands emulate old-style tactical theorem proving.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: