author oheimb Fri, 25 Sep 1998 16:21:56 +0200 changeset 5577 ddaa1c133c5a parent 5576 dc6ee60d2be8 child 5578 7de426cf179c
minor corrections
 doc-src/Ref/classical.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Ref/classical.tex	Fri Sep 25 15:57:23 1998 +0200
+++ b/doc-src/Ref/classical.tex	Fri Sep 25 16:21:56 1998 +0200
@@ -4,9 +4,9 @@
\newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}

Although Isabelle is generic, many users will be working in some
-extension of classical first-order logic.  Isabelle's set theory~{\tt
-  ZF} is built upon theory~\texttt{FOL}, while {\HOL}
-conceptually contains first-order logic as a fragment.
+extension of classical first-order logic.
+Isabelle's set theory~{\tt ZF} is built upon theory~\texttt{FOL},
+while {\HOL} conceptually contains first-order logic as a fragment.
Theorem-proving in predicate logic is undecidable, but many
researchers have developed strategies to assist in this task.

@@ -530,8 +530,8 @@
form $x=t$ may be eliminated.  The user-supplied safe wrapper tactical is
applied.
\item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but
-also does simplification with the given simpset. Still note that if the simpset
-includes a splitter for the premises, the subgoal may be split.
+also does simplification with the given simpset. note that if the simpset
+includes a splitter for the premises, the subgoal may still be split.
\end{ttdescription}

@@ -675,7 +675,7 @@
\label{sec:access-current-claset}

the functions to access the current claset are analogous to the functions
-for the current simpset, so please see \label{sec:access-current-simpset}
+for the current simpset, so please see \ref{sec:access-current-simpset}
for a description.
\begin{ttbox}
claset        : unit   -> claset
@@ -685,7 +685,6 @@
print_claset  : theory -> unit
CLASET        :(claset     ->       tactic) ->       tactic
CLASET'       :(claset     -> 'a -> tactic) -> 'a -> tactic
-
CLASIMPSET    :(clasimpset ->       tactic) ->       tactic
CLASIMPSET'   :(clasimpset -> 'a -> tactic) -> 'a -> tactic
\end{ttbox}