%% $Id$

\documentclass[12pt,a4paper,fleqn]{report}

\usepackage{latexsym,graphicx,../iman,../extra,../ttbox,../proof,../rail,../railsetup,../isar,../pdfsetup}

\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}

\author{\emph{Markus Wenzel} \\ TU M\"unchen}

\makeindex

\newcommand{\isastyle}{\small\tt\slshape}

\newcommand{\isa}[1]{\emph{\isastyle #1}}

\newcommand{\isamath}[1]{\emph{$#1$}}

\newcommand{\isasymColon}{\isamath{\mathrel{::}}}

\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}

\railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}

\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}

\railterm{name,nameref,text,type,term,prop,atom}

\railalias{ident}{\railtoken{ident}}

\railalias{longident}{\railtoken{longident}}

\railalias{symident}{\railtoken{symident}}

\railalias{var}{\railtoken{var}}

\railalias{textvar}{\railtoken{textvar}}

\railalias{typefree}{\railtoken{typefree}}

\railalias{typevar}{\railtoken{typevar}}

\railalias{nat}{\railtoken{nat}}

\railalias{string}{\railtoken{string}}

\railalias{verbatim}{\railtoken{verbatim}}

\railalias{keyword}{\railtoken{keyword}}

\railalias{name}{\railqtoken{name}}

\railalias{nameref}{\railqtoken{nameref}}

\railalias{text}{\railqtoken{text}}

\railalias{type}{\railqtoken{type}}

\railalias{term}{\railqtoken{term}}

\railalias{prop}{\railqtoken{prop}}

\railalias{atom}{\railqtoken{atom}}

\newcommand{\drv}{\mathrel{\vdash}}

\newcommand{\edrv}{\mathop{\drv}\nolimits}

\newcommand{\Or}{\mathrel{\;|\;}}

\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}

\pagestyle{headings}

\sloppy

\binperiod     %%%treat . like a binary operator

\renewcommand{\phi}{\varphi}

%\includeonly{}

\begin{document}

\underscoreoff

\maketitle 

\begin{abstract}

  \emph{Intelligible semi-automated reasoning} (\emph{Isar}) is a generic

  approach to readable formal proof documents.  It sets out to bridge the

  semantic gap between any internal notions of proof based on primitive

  inferences and tactics, and an appropriate level of abstraction for

  user-level work.  The Isar formal proof language has been designed to

  satisfy quite contradictory requirements, being both ``declarative'' and

  immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter.

  The Isabelle/Isar system provides an interpreter for the Isar formal proof

  language.  The input may consist either of proper document constructors, or

  improper auxiliary commands (for diagnostics, exploration etc.).  Proof

  texts consisting of proper elements only admit a purely static reading, thus

  being intelligible later without requiring dynamic replay that is so typical

  for traditional proof scripts.  Any of the Isabelle/Isar commands may be

  executed in single-steps, so basically the interpreter has a proof text

  debugger already built-in.

  Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs

  interface for interactive proof assistants, we arrive at a reasonable

  environment for \emph{live document editing}.  Thus proof texts may be

  developed incrementally by issuing proof commands, including forward and

  backward tracing of partial documents; intermediate states may be inspected

  by diagnostic commands.

  The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic

  implementation.  Theories, theorems, proof procedures etc.\ may be used

  interchangeably between classic Isabelle proof scripts and Isabelle/Isar

  documents.  Even more, Isar provides a set of emulation commands and methods

  for simulating traditional tactic scripts within new-style theory documents.

  The Isar framework is as generic as Isabelle, able to support a wide range

  of object-logics.  Currently, the end-user working environment is most

  complete for Isabelle/HOL.

\end{abstract}

\pagenumbering{roman} \tableofcontents \clearfirst

%FIXME

\nocite{Aspinall:2000:eProof}

\nocite{Bauer-Wenzel:2000:HB}

\nocite{Harrison:1996:MizarHOL}

\nocite{Muzalewski:Mizar}

\nocite{Rudnicki:1992:MizarOverview}

\nocite{Rudnicki:1992:MizarOverview}

\nocite{Syme:1997:DECLARE}

\nocite{Syme:1998:thesis}

\nocite{Syme:1999:TPHOL}

\nocite{Trybulec:1993:MizarFeatures}

\nocite{Wiedijk:1999:Mizar}

\nocite{Wiedijk:2000:MV}

\nocite{Zammit:1999:TPHOL}

\include{intro}

\include{basics}

\include{syntax}

\include{pure}

\include{generic}

\include{hol}

\appendix

\include{refcard}

\include{conversion}

\begingroup

  \bibliographystyle{plain} \small\raggedright\frenchspacing

  \bibliography{../manual}

\endgroup

\printindex

\end{document}