(1) signatures updated according to normalizer_data.ML (added field ideal in entry);
(2) For a theory the conversions returned are now ring_conv (as before, proves a universal statement), simple_ideal proves ideal membership for one polynomial ; multi_ideal solves the more general ideal membership for several existentially quantifier variables involved in several conjunctions; a simpset containing a simproc to turn x = y into p = 0 where p is the normal form of x - y;
(3) Added ideal_tac a tactic to prove general ideal membership (cf. John Harrision CADE 2007) ;
(4) Added algebra_tac : first tries ring_tac (old algebra) then ideal_tac
%% $Id$
\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{latexsym,graphicx}
\usepackage[refpage]{nomencl}
\usepackage{../iman,../extra,../isar,../proof}
\usepackage{Thy/document/isabelle,Thy/document/isabellesym}
\usepackage{style}
\usepackage{../pdfsetup}
\hyphenation{Isabelle}
\hyphenation{Isar}
\isadroptag{theory}
\title{\includegraphics[scale=0.5]{isabelle_isar}
\\[4ex] The Isabelle/Isar Implementation}
\author{\emph{Makarius Wenzel}}
%FIXME
%\makeglossary
\makeindex
\begin{document}
\maketitle
\begin{abstract}
We describe the key concepts underlying the Isabelle/Isar
implementation, including ML references for the most important
functions. The aim is to give some insight into the overall system
architecture, and provide clues on implementing applications within
this framework.
\end{abstract}
\vspace*{2.5cm}
\begin{quote}
{\small\em Isabelle was not designed; it evolved. Not everyone
likes this idea. Specification experts rightly abhor
trial-and-error programming. They suggest that no one should
write a program without first writing a complete formal
specification. But university departments are not software houses.
Programs like Isabelle are not products: when they have served
their purpose, they are discarded.}
Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
\vspace*{1cm}
{\small\em As I did 20 years ago, I still fervently believe that the
only way to make software secure, reliable, and fast is to make it
small. Fight features.}
Andrew S. Tanenbaum
\end{quote}
\thispagestyle{empty}\clearpage
\pagenumbering{roman}
\tableofcontents
\listoffigures
\clearfirst
%\input{intro.tex}
\input{Thy/document/prelim.tex}
\input{Thy/document/logic.tex}
\input{Thy/document/tactic.tex}
\input{Thy/document/proof.tex}
\input{Thy/document/isar.tex}
\input{Thy/document/locale.tex}
\input{Thy/document/integration.tex}
\appendix
\input{Thy/document/ML.tex}
\begingroup
\tocentry{\bibname}
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{../manual}
\endgroup
%FIXME
%\tocentry{\glossaryname}
%\printglossary
\tocentry{\indexname}
\printindex
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: