wenzelm@7046: 
wenzelm@7046: %% $Id$
wenzelm@7046: 
wenzelm@7836: \documentclass[12pt,a4paper,fleqn]{report}
wenzelm@7974: \usepackage{latexsym,graphicx,../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@7895: \newcommand{\drv}{\mathrel{\vdash}}
wenzelm@7895: \newcommand{\edrv}{\mathop{\drv}\nolimits}
wenzelm@7974: \newcommand{\Or}{\mathrel{\;|\;}}
wenzelm@7895: 
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@7974: %\includeonly{refcard}
wenzelm@7895: 
wenzelm@7895: 
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@7895:   interface layer.  The Isabelle/Isar system provides an interpreter for the
wenzelm@7981:   Isar formal proof document language.  The input may consist either of proper
wenzelm@7981:   document constructors, or improper auxiliary commands (for diagnostics,
wenzelm@7981:   exploration etc.).  Proof texts consisting of proper document constructors
wenzelm@7981:   only, admit a purely static reading, thus being intelligible later without
wenzelm@7981:   requiring dynamic replay that is so typical for traditional proof scripts.
wenzelm@7981:   Any of the Isabelle/Isar commands may be executed in single-steps, so
wenzelm@7981:   basically the interpreter has a proof text debugger already built-in.
wenzelm@7167:   
wenzelm@7297:   Employing the Isar instantiation of \emph{Proof~General}, 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@7335:   The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
wenzelm@7335:   implementation.  Theories, theorems, proof procedures etc.\ may be used
wenzelm@7895:   interchangeably between classic Isabelle proof scripts and Isabelle/Isar
wenzelm@7335:   documents.  Isar is as generic as Isabelle, able to support a wide range of
wenzelm@7895:   object-logics.  Currently, the end-user working environment is most complete
wenzelm@7895:   for 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@7988: \nocite{Zammit: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@7895: \appendix
wenzelm@7895: \include{refcard}
wenzelm@7895: 
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}