wenzelm@7046: 
wenzelm@7046: %% $Id$
wenzelm@7046: 
wenzelm@7134: \documentclass[12pt,fleqn]{report}
wenzelm@7134: \usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}
wenzelm@7046: 
wenzelm@7046: \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
wenzelm@7050: \author{\emph{Markus Wenzel} \\ TU M\"unchen}
wenzelm@7046: 
wenzelm@7050: \makeindex
wenzelm@7050: 
wenzelm@7167: \railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}
wenzelm@7167: \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
wenzelm@7134: 
wenzelm@7134: \railalias{name}{\railqtoken{name}}
wenzelm@7134: \railalias{nameref}{\railqtoken{nameref}}
wenzelm@7134: \railalias{text}{\railqtoken{text}}
wenzelm@7134: \railalias{type}{\railqtoken{type}}
wenzelm@7134: \railalias{term}{\railqtoken{term}}
wenzelm@7134: \railalias{prop}{\railqtoken{prop}}
wenzelm@7134: \railalias{atom}{\railqtoken{atom}}
wenzelm@7134: 
wenzelm@7046: 
wenzelm@7046: \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
wenzelm@7046: 
wenzelm@7046: \pagestyle{headings}
wenzelm@7046: \sloppy
wenzelm@7046: \binperiod     %%%treat . like a binary operator
wenzelm@7046: 
wenzelm@7134: \renewcommand{\phi}{\varphi}
wenzelm@7046: 
wenzelm@7046: 
wenzelm@7046: \begin{document}
wenzelm@7046: 
wenzelm@7046: \underscoreoff
wenzelm@7046: 
wenzelm@7046: \maketitle 
wenzelm@7046: 
wenzelm@7046: \begin{abstract}
wenzelm@7167:   \emph{Intelligible semi-automated reasoning} (\emph{Isar}) is a generic
wenzelm@7167:   approach to readable formal proof documents.  It sets out to bridge the
wenzelm@7167:   semantic gap between any internal notions of proof based on primitive
wenzelm@7167:   inferences and tactics, and an appropriate level of abstraction for
wenzelm@7167:   user-level work.  The Isar formal proof language has been designed to
wenzelm@7167:   satisfy quite contradictory requirements, being both ``declarative'' and
wenzelm@7167:   immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter.
wenzelm@7167:   
wenzelm@7167:   The current version of Isabelle offers Isar as an alternative proof language
wenzelm@7167:   interface layer, beyond traditional tactic scripts.  The Isabelle/Isar
wenzelm@7167:   system provides an interpreter for the Isar formal proof document language.
wenzelm@7167:   Isabelle/Isar input may consist either of \emph{proper document
wenzelm@7167:     constructors}, or \emph{improper auxiliary commands} (for diagnostics,
wenzelm@7167:   exploration etc.).  Proof texts consisting of proper document constructors
wenzelm@7167:   only admit a purely static reading, thus being intelligible later without
wenzelm@7167:   requiring dynamic replay that is so typical for traditional proof scripts.
wenzelm@7167:   Any of the Isabelle/Isar commands may be executed in single-steps, so
wenzelm@7167:   basically the interpreter has a proof text debugger already built-in.
wenzelm@7167:   
wenzelm@7167:   Employing the \emph{ProofGeneral/isar} instantiation of the generic Emacs
wenzelm@7167:   interface for interactive proof assistants of LFCS Edinburgh, we arrive at a
wenzelm@7167:   reasonable environment for \emph{live document editing}.  Thus proof texts
wenzelm@7167:   may be developed incrementally by issuing proper document constructors,
wenzelm@7167:   including forward and backward tracing of partial documents; intermediate
wenzelm@7167:   states may be inspected by diagnostic commands.
wenzelm@7167:   
wenzelm@7167:   The Isar subsystem of Isabelle is tightly integrated into the Isabelle/Pure
wenzelm@7167:   meta-logic implementation.  Theories, theorems, proof procedures etc.\ may
wenzelm@7167:   be used interchangeably between Isabelle-classic proof scripts and
wenzelm@7167:   Isabelle/Isar documents.  Isar is as generic as Isabelle, able to support a
wenzelm@7167:   wide range of object-logics.  The current end-user setup is mainly for
wenzelm@7167:   Isabelle/HOL.
wenzelm@7046: \end{abstract}
wenzelm@7046: 
wenzelm@7046: \pagenumbering{roman} \tableofcontents \clearfirst
wenzelm@7046: 
wenzelm@7046: %FIXME
wenzelm@7046: \nocite{Rudnicki:1992:MizarOverview}
wenzelm@7046: \nocite{Harrison:1996:MizarHOL}
wenzelm@7046: \nocite{Rudnicki:1992:MizarOverview}
wenzelm@7046: \nocite{Trybulec:1993:MizarFeatures}
wenzelm@7046: \nocite{Syme:1997:DECLARE}
wenzelm@7046: \nocite{Syme:1998:thesis}
wenzelm@7046: \nocite{Syme:1999:TPHOL}
wenzelm@7046: \nocite{Wenzel:1999:TPHOL}
wenzelm@7046: 
wenzelm@7046: \include{intro}
wenzelm@7046: \include{basics}
wenzelm@7046: \include{syntax}
wenzelm@7046: \include{pure}
wenzelm@7135: \include{generic}
wenzelm@7046: \include{hol}
wenzelm@7046: 
wenzelm@7046: \begingroup
wenzelm@7046:   \bibliographystyle{plain} \small\raggedright\frenchspacing
wenzelm@7046:   \bibliography{../manual}
wenzelm@7046: \endgroup
wenzelm@7046: 
wenzelm@7046: \input{isar-ref.ind}
wenzelm@7046: 
wenzelm@7046: \end{document}