--- a/doc-src/Ref/goals.tex Wed May 07 16:26:28 1997 +0200
+++ b/doc-src/Ref/goals.tex Wed May 07 16:29:06 1997 +0200
@@ -393,13 +393,15 @@
\section{Executing batch proofs}
-\index{batch execution}
+\index{batch execution}%
+To save space below, let type \texttt{tacfun} abbreviate \texttt{thm list ->
+ tactic list}, which is the type of a tactical proof.
\begin{ttbox}
-prove_goal : theory-> string->(thm list->tactic list)->thm
-qed_goal : string->theory-> string->(thm list->tactic list)->unit
-prove_goalw: theory->thm list->string->(thm list->tactic list)->thm
-qed_goalw : string->theory->thm list->string->(thm list->tactic list)->unit
-prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm
+prove_goal : theory -> string -> tacfun -> thm
+qed_goal : string -> theory -> string -> tacfun -> unit
+prove_goalw: theory -> thm list -> string -> tacfun -> thm
+qed_goalw : string -> theory -> thm list -> string -> tacfun -> unit
+prove_goalw_cterm: thm list -> cterm -> tacfun -> thm
\end{ttbox}
These batch functions create an initial proof state, then apply a tactic to
it, yielding a sequence of final proof states. The head of the sequence is
--- a/doc-src/Ref/ref.tex Wed May 07 16:26:28 1997 +0200
+++ b/doc-src/Ref/ref.tex Wed May 07 16:29:06 1997 +0200
@@ -1,9 +1,8 @@
\documentclass[12pt]{report}
-\usepackage{a4}
+\usepackage{a4,proof}
\makeatletter
\input{../rail.sty}
-\input{../proof.sty}
\input{../iman.sty}
\input{../extra.sty}
\makeatother
@@ -16,19 +15,19 @@
%%% needs chapter on Provers/typedsimp.ML?
\title{The Isabelle Reference Manual}
-\author{{\em Lawrence C. Paulson}%
+\author{{\em Lawrence C. Paulson}\\
+ Computer Laboratory \\ University of Cambridge \\
+ \texttt{lcp@cl.cam.ac.uk}\\[3ex]
+ With Contributions by Tobias Nipkow and Markus Wenzel%
\thanks{Tobias Nipkow, of T. U. Munich, wrote most of
Chapters~\protect\ref{Defining-Logics} and~\protect\ref{simp-chap}, and part of
Chapter~\protect\ref{theories}. Carsten Clasohm also contributed to
Chapter~\protect\ref{theories}. Markus Wenzel contributed to
Chapter~\protect\ref{chap:syntax}. Sara Kalvala, Martin Simons and others
suggested changes
- and corrections. The research has been funded by the SERC (grants
- GR/G53279, GR/H40570) and by ESPRIT project 6453: Types.}
-\\
-Computer Laboratory \\ University of Cambridge \\[2ex]
-\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}\\[3cm]
-Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
+ and corrections. The research has been funded by the EPSRC (grants
+ GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT project 6453:
+ Types.}}
\makeindex
--- a/doc-src/Ref/simplifier.tex Wed May 07 16:26:28 1997 +0200
+++ b/doc-src/Ref/simplifier.tex Wed May 07 16:29:06 1997 +0200
@@ -269,7 +269,7 @@
The solver is a pair of tactics that attempt to solve a subgoal after
simplification. Typically it just proves trivial subgoals such as {\tt
True} and $t=t$. It could use sophisticated means such as {\tt
- fast_tac}, though that could make simplification expensive.
+ blast_tac}, though that could make simplification expensive.
Rewriting does not instantiate unknowns. For example, rewriting
cannot prove $a\in \Var{A}$ since this requires
@@ -306,7 +306,7 @@
should call the simplifier at some point. The simplifier will then call the
solver, which must therefore be prepared to solve goals of the form $t =
\Var{x}$, usually by reflexivity. In particular, reflexivity should be
-tried before any of the fancy tactics like {\tt fast_tac}.
+tried before any of the fancy tactics like {\tt blast_tac}.
It may even happen that due to simplification the subgoal is no longer
an equality. For example $False \bimp \Var{Q}$ could be rewritten to
@@ -366,14 +366,16 @@
\index{*Asm_full_simp_tac}
\begin{ttbox}
-infix 4 setsubgoaler setloop addloop setSSolver addSSolver setSolver addSolver
+infix 4 setsubgoaler setloop addloop
+ setSSolver addSSolver setSolver addSolver
setmksimps addsimps delsimps addeqcongs deleqcongs;
signature SIMPLIFIER =
sig
type simpset
val empty_ss: simpset
- val rep_ss: simpset -> {simps: thm list, procs: string list, congs: thm list,
+ val rep_ss: simpset -> {simps: thm list, procs: string list,
+ congs: thm list,
subgoal_tac: simpset -> int -> tactic,
loop_tac: int -> tactic,
finish_tac: thm list -> int -> tactic,
@@ -758,7 +760,7 @@
\begin{ttbox}
2 * sum (\%i. i) (Suc n) = n * Suc n
1. !!n1. n1 + sum (\%i. i) n1 + (n1 + sum (\%i. i) n1) = n1 + n1 * n1
- ==> n1 + (n1 + sum (\%i. i) n1) + (n1 + (n1 + sum (\%i. i) n1)) =
+ ==> n1 + (n1 + sum (\%i. i) n1) + (n1 + (n1 + sum (\%i.i) n1)) =
n1 + (n1 + (n1 + n1 * n1))
\end{ttbox}
Ordered rewriting proves this by sorting the left-hand side. Proving
@@ -774,7 +776,7 @@
signs:
\begin{ttbox}
val symmetry = prove_goal HOL.thy "(x=y) = (y=x)"
- (fn _ => [fast_tac HOL_cs 1]);
+ (fn _ => [Blast_tac 1]);
\end{ttbox}
This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs
in the conclusion but not~$s$, can often be brought into the right form.
--- a/doc-src/Ref/substitution.tex Wed May 07 16:26:28 1997 +0200
+++ b/doc-src/Ref/substitution.tex Wed May 07 16:29:06 1997 +0200
@@ -126,11 +126,11 @@
sig
structure Simplifier : SIMPLIFIER
val dest_eq : term -> term*term
- val eq_reflection : thm (* a=b ==> a==b *)
- val imp_intr : thm (* (P ==> Q) ==> P-->Q *)
- val rev_mp : thm (* [| P; P-->Q |] ==> Q *)
- val subst : thm (* [| a=b; P(a) |] ==> P(b) *)
- val sym : thm (* a=b ==> b=a *)
+ val eq_reflection : thm (* a=b ==> a==b *)
+ val imp_intr : thm (* (P ==> Q) ==> P-->Q *)
+ val rev_mp : thm (* [| P; P-->Q |] ==> Q *)
+ val subst : thm (* [| a=b; P(a) |] ==> P(b) *)
+ val sym : thm (* a=b ==> b=a *)
end;
\end{ttbox}
Thus, the functor requires the following items:
--- a/doc-src/Ref/syntax.tex Wed May 07 16:26:28 1997 +0200
+++ b/doc-src/Ref/syntax.tex Wed May 07 16:29:06 1997 +0200
@@ -813,7 +813,7 @@
if 0 mem (loose_bnos B) then
let val (x', B') = Syntax.variant_abs' (x, dummyT, B) in
list_comb
- (Const (q, dummyT) $ Syntax.mark_boundT (x', T) $ A $ B', ts)
+ (Const (q,dummyT) $ Syntax.mark_boundT (x', T) $ A $ B', ts)
end
else list_comb (Const (r, dummyT) $ A $ B, ts)
| dependent_tr' _ _ = raise Match;