--- a/src/Doc/ProgProve/Bool_nat_list.thy Tue Nov 19 22:20:01 2013 +0100
+++ b/src/Doc/ProgProve/Bool_nat_list.thy Wed Nov 20 08:56:54 2013 +0100
@@ -99,10 +99,10 @@
For example, given the goal @{text"x + 0 = x"}, there is nothing to indicate
that you are talking about natural numbers. Hence Isabelle can only infer
that @{term x} is of some arbitrary type where @{text 0} and @{text"+"}
- exist. As a consequence, you will be unable to prove the
- goal. To alert you to such pitfalls, Isabelle flags numerals without a
- fixed type in its output: @{prop"x+0 = x"}. In this particular example,
- you need to include
+ exist. As a consequence, you will be unable to prove the goal.
+% To alert you to such pitfalls, Isabelle flags numerals without a
+% fixed type in its output: @ {prop"x+0 = x"}.
+ In this particular example, you need to include
an explicit type constraint, for example @{text"x+0 = (x::nat)"}. If there
is enough contextual information this may not be necessary: @{prop"Suc x =
x"} automatically implies @{text"x::nat"} because @{term Suc} is not
--- a/src/Doc/ProgProve/document/intro-isabelle.tex Tue Nov 19 22:20:01 2013 +0100
+++ b/src/Doc/ProgProve/document/intro-isabelle.tex Wed Nov 20 08:56:54 2013 +0100
@@ -16,7 +16,7 @@
of recursive functions.
\ifsem
\autoref{sec:CaseStudyExp} contains a
-little case study: arithmetic and boolean expressions, their evaluation,
+small case study: arithmetic and boolean expressions, their evaluation,
optimization and compilation.
\fi
\autoref{ch:Logic} introduces the rest of HOL: the
@@ -35,8 +35,8 @@
% in the intersection of computation and logic.
This introduction to the core of Isabelle is intentionally concrete and
-example-based: we concentrate on examples that illustrate the typical cases;
-we do not explain the general case if it can be inferred from the examples.
+example-based: we concentrate on examples that illustrate the typical cases
+without explaining the general case if it can be inferred from the examples.
We cover the essentials (from a functional programming point of view) as
quickly and compactly as possible.
\ifsem
@@ -46,7 +46,7 @@
For a comprehensive treatment of all things Isabelle we recommend the
\emph{Isabelle/Isar Reference Manual}~\cite{IsarRef}, which comes with the
Isabelle distribution.
-The tutorial by Nipkow, Paulson and Wenzel~\cite{LNCS2283} (in its updated version that comes with the Isabelle distribution) is still recommended for the wealth of examples and material, but its proof style is outdated. In particular it fails to cover the structured proof language Isar.
+The tutorial by Nipkow, Paulson and Wenzel~\cite{LNCS2283} (in its updated version that comes with the Isabelle distribution) is still recommended for the wealth of examples and material, but its proof style is outdated. In particular it does not cover the structured proof language Isar.
%This introduction to Isabelle has grown out of many years of teaching
%Isabelle courses.