doc-src/IsarRef/isar-ref.tex
changeset 7466 7df66ce6508a
parent 7335 abba35b98892
child 7509 d6fc3c4423f7
equal deleted inserted replaced
7465:a987f4ff5bd3 7466:7df66ce6508a
    65   
    65   
    66   The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
    66   The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
    67   implementation.  Theories, theorems, proof procedures etc.\ may be used
    67   implementation.  Theories, theorems, proof procedures etc.\ may be used
    68   interchangeably between Isabelle-classic proof scripts and Isabelle/Isar
    68   interchangeably between Isabelle-classic proof scripts and Isabelle/Isar
    69   documents.  Isar is as generic as Isabelle, able to support a wide range of
    69   documents.  Isar is as generic as Isabelle, able to support a wide range of
    70   object-logics.  The current end-user setup is mainly for Isabelle/HOL.
    70   object-logics.  The current working environment for end-users is setup
       
    71   mainly for Isabelle/HOL.
    71 \end{abstract}
    72 \end{abstract}
    72 
    73 
    73 \pagenumbering{roman} \tableofcontents \clearfirst
    74 \pagenumbering{roman} \tableofcontents \clearfirst
    74 
    75 
    75 %FIXME
    76 %FIXME
    78 \nocite{Rudnicki:1992:MizarOverview}
    79 \nocite{Rudnicki:1992:MizarOverview}
    79 \nocite{Trybulec:1993:MizarFeatures}
    80 \nocite{Trybulec:1993:MizarFeatures}
    80 \nocite{Syme:1997:DECLARE}
    81 \nocite{Syme:1997:DECLARE}
    81 \nocite{Syme:1998:thesis}
    82 \nocite{Syme:1998:thesis}
    82 \nocite{Syme:1999:TPHOL}
    83 \nocite{Syme:1999:TPHOL}
    83 \nocite{Wenzel:1999:TPHOL}
       
    84 
    84 
    85 \include{intro}
    85 \include{intro}
    86 \include{basics}
    86 \include{basics}
    87 \include{syntax}
    87 \include{syntax}
    88 \include{pure}
    88 \include{pure}