doc-src/IsarRef/isar-ref.tex

fixed term syntax;

%% $Id$

\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{latexsym,graphicx,../iman,../extra,../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

\railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}
\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,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{generic,refcard}


\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 current version of Isabelle offers Isar as an alternative proof language
  interface layer.  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.  Isar 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
% - HahnBanach paper
% - Freek Widijk's stuff

%FIXME
\nocite{Rudnicki:1992:MizarOverview}
\nocite{Harrison:1996:MizarHOL}
\nocite{Rudnicki:1992:MizarOverview}
\nocite{Trybulec:1993:MizarFeatures}
\nocite{Syme:1997:DECLARE}
\nocite{Syme:1998:thesis}
\nocite{Syme:1999:TPHOL}
\nocite{Zammit:1999:TPHOL}

\include{intro}
\include{basics}
\include{syntax}
\include{pure}
\include{generic}
\include{hol}

\appendix
\include{refcard}

\begingroup
  \bibliographystyle{plain} \small\raggedright\frenchspacing
  \bibliography{../manual}
\endgroup

\input{isar-ref.ind}

\end{document}