author paulson Wed, 07 May 1997 16:26:28 +0200 changeset 3127 4cc2fe62f7c3 parent 3126 feb7a5d01c1e child 3128 d01d4c0c4b44
New acknowledgements; no Fast_tac
 doc-src/Intro/getting.tex file | annotate | diff | comparison | revisions doc-src/Intro/intro.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Intro/getting.tex	Wed May 07 16:26:02 1997 +0200
+++ b/doc-src/Intro/getting.tex	Wed May 07 16:26:28 1997 +0200
@@ -883,7 +883,7 @@
Rules are packaged into {\bf classical sets}.  The classical reasoner
provides several tactics, which apply rules using naive algorithms.
Unification handles quantifiers as shown above.  The most useful tactic
-is~\ttindex{fast_tac}.
+is~\ttindex{Blast_tac}.

Let us solve problems~40 and~60 of Pelletier~\cite{pelletier86}.  (The
backslashes~\hbox{\verb|\|\ldots\verb|\|} are an \ML{} string escape
@@ -897,10 +897,11 @@
{\out  1. (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
{\out     ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
\end{ttbox}
-The rules of classical logic are bundled as {\tt FOL_cs}.  We may solve
-subgoal~1 at a stroke, using~\ttindex{fast_tac}.
+\ttindex{Blast_tac} proves subgoal~1 at a stroke.
\begin{ttbox}
-by (fast_tac FOL_cs 1);
+by (Blast_tac 1);
+{\out Depth = 0}
+{\out Depth = 1}
{\out Level 1}
{\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
@@ -919,7 +920,9 @@
\end{ttbox}
Again, subgoal~1 succumbs immediately.
\begin{ttbox}
-by (fast_tac FOL_cs 1);
+by (Blast_tac 1);
+{\out Depth = 0}
+{\out Depth = 1}
{\out Level 1}
{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
{\out No subgoals!}
--- a/doc-src/Intro/intro.tex	Wed May 07 16:26:02 1997 +0200
+++ b/doc-src/Intro/intro.tex	Wed May 07 16:26:28 1997 +0200
@@ -1,8 +1,7 @@
\documentclass[12pt]{article}
-\usepackage{a4}
+\usepackage{a4,proof}

\makeatletter
-\input{../proof.sty}
\input{../iman.sty}
\input{../extra.sty}
\makeatother
@@ -15,8 +14,9 @@

\title{Introduction to Isabelle}
\author{{\em Lawrence C. Paulson}\\
-        Computer Laboratory \\ University of Cambridge \\[2ex]
-        {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}}
+        Computer Laboratory \\ University of Cambridge \\
+        \texttt{lcp@cl.cam.ac.uk}\\[3ex]
+        With Contributions by Tobias Nipkow and Markus Wenzel
}
\makeindex

@@ -106,7 +106,7 @@

\subsubsection*{Acknowledgements}
Tobias Nipkow contributed most of the section on defining theories.
-Stefan Berghofer, Sara Kalvala and Markus Wenzel suggested improvements.
+Stefan Berghofer and Sara Kalvala suggested improvements.

Tobias Nipkow has made immense contributions to Isabelle, including the
parser generator, type classes, and the simplifier.  Carsten Clasohm and
@@ -114,9 +114,9 @@
also helped.  Isabelle was developed using Dave Matthews's Standard~{\sc
ml} compiler, Poly/{\sc ml}.  Many people have contributed to Isabelle's
standard object-logics, including Martin Coen, Philippe de Groote, Philippe
-No\"el.  The research has been funded by the SERC (grants GR/G53279,
-GR/H40570) and by ESPRIT (projects 3245: Logical Frameworks, and 6453:
-Types).
+No\"el.  The research has been funded by the EPSRC (grants
+GR/G53279, GR/H40570, GR/K57381, GR/K77051)
+and by ESPRIT (projects 3245: Logical Frameworks, and 6453: Types).

\newpage
\pagestyle{plain} \tableofcontents