# HG changeset patch
# User paulson
# Date 863015188 -7200
# Node ID 4cc2fe62f7c321910ae23a6ebf5aa68518fe5088
# Parent  feb7a5d01c1e2b017285c66556c855a8f2d6b7d6
New acknowledgements; no Fast_tac

diff -r feb7a5d01c1e -r 4cc2fe62f7c3 doc-src/Intro/getting.tex
--- 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!}
diff -r feb7a5d01c1e -r 4cc2fe62f7c3 doc-src/Intro/intro.tex
--- 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