New acknowledgements; no Fast_tac
authorpaulson
Wed May 07 16:26:28 1997 +0200 (1997-05-07)
changeset 31274cc2fe62f7c3
parent 3126 feb7a5d01c1e
child 3128 d01d4c0c4b44
New acknowledgements; no Fast_tac
doc-src/Intro/getting.tex
doc-src/Intro/intro.tex
     1.1 --- a/doc-src/Intro/getting.tex	Wed May 07 16:26:02 1997 +0200
     1.2 +++ b/doc-src/Intro/getting.tex	Wed May 07 16:26:28 1997 +0200
     1.3 @@ -883,7 +883,7 @@
     1.4  Rules are packaged into {\bf classical sets}.  The classical reasoner
     1.5  provides several tactics, which apply rules using naive algorithms.
     1.6  Unification handles quantifiers as shown above.  The most useful tactic
     1.7 -is~\ttindex{fast_tac}.  
     1.8 +is~\ttindex{Blast_tac}.  
     1.9  
    1.10  Let us solve problems~40 and~60 of Pelletier~\cite{pelletier86}.  (The
    1.11  backslashes~\hbox{\verb|\|\ldots\verb|\|} are an \ML{} string escape
    1.12 @@ -897,10 +897,11 @@
    1.13  {\out  1. (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
    1.14  {\out     ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
    1.15  \end{ttbox}
    1.16 -The rules of classical logic are bundled as {\tt FOL_cs}.  We may solve
    1.17 -subgoal~1 at a stroke, using~\ttindex{fast_tac}.
    1.18 +\ttindex{Blast_tac} proves subgoal~1 at a stroke.
    1.19  \begin{ttbox}
    1.20 -by (fast_tac FOL_cs 1);
    1.21 +by (Blast_tac 1);
    1.22 +{\out Depth = 0}
    1.23 +{\out Depth = 1}
    1.24  {\out Level 1}
    1.25  {\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
    1.26  {\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
    1.27 @@ -919,7 +920,9 @@
    1.28  \end{ttbox}
    1.29  Again, subgoal~1 succumbs immediately.
    1.30  \begin{ttbox}
    1.31 -by (fast_tac FOL_cs 1);
    1.32 +by (Blast_tac 1);
    1.33 +{\out Depth = 0}
    1.34 +{\out Depth = 1}
    1.35  {\out Level 1}
    1.36  {\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
    1.37  {\out No subgoals!}
     2.1 --- a/doc-src/Intro/intro.tex	Wed May 07 16:26:02 1997 +0200
     2.2 +++ b/doc-src/Intro/intro.tex	Wed May 07 16:26:28 1997 +0200
     2.3 @@ -1,8 +1,7 @@
     2.4  \documentclass[12pt]{article}
     2.5 -\usepackage{a4}
     2.6 +\usepackage{a4,proof}
     2.7  
     2.8  \makeatletter
     2.9 -\input{../proof.sty}
    2.10  \input{../iman.sty}
    2.11  \input{../extra.sty}
    2.12  \makeatother
    2.13 @@ -15,8 +14,9 @@
    2.14  
    2.15  \title{Introduction to Isabelle}   
    2.16  \author{{\em Lawrence C. Paulson}\\
    2.17 -        Computer Laboratory \\ University of Cambridge \\[2ex]
    2.18 -        {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}}
    2.19 +        Computer Laboratory \\ University of Cambridge \\
    2.20 +        \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
    2.21 +        With Contributions by Tobias Nipkow and Markus Wenzel
    2.22  }
    2.23  \makeindex
    2.24  
    2.25 @@ -106,7 +106,7 @@
    2.26  
    2.27  \subsubsection*{Acknowledgements} 
    2.28  Tobias Nipkow contributed most of the section on defining theories.
    2.29 -Stefan Berghofer, Sara Kalvala and Markus Wenzel suggested improvements.
    2.30 +Stefan Berghofer and Sara Kalvala suggested improvements.
    2.31  
    2.32  Tobias Nipkow has made immense contributions to Isabelle, including the
    2.33  parser generator, type classes, and the simplifier.  Carsten Clasohm and
    2.34 @@ -114,9 +114,9 @@
    2.35  also helped.  Isabelle was developed using Dave Matthews's Standard~{\sc
    2.36    ml} compiler, Poly/{\sc ml}.  Many people have contributed to Isabelle's
    2.37  standard object-logics, including Martin Coen, Philippe de Groote, Philippe
    2.38 -No\"el.  The research has been funded by the SERC (grants GR/G53279,
    2.39 -GR/H40570) and by ESPRIT (projects 3245: Logical Frameworks, and 6453:
    2.40 -Types).
    2.41 +No\"el.  The research has been funded by the EPSRC (grants
    2.42 +GR/G53279, GR/H40570, GR/K57381, GR/K77051)
    2.43 +and by ESPRIT (projects 3245: Logical Frameworks, and 6453: Types).
    2.44  
    2.45  \newpage
    2.46  \pagestyle{plain} \tableofcontents