# HG changeset patch
# User nipkow
# Date 1384934214 -3600
# Node ID 4bc48d7136026cb49c7b24f47f735d6ee0f03c18
# Parent  d983a020489dd0362594dfd45a6066c950d764b6
tuned

diff -r d983a020489d -r 4bc48d713602 src/Doc/ProgProve/Bool_nat_list.thy
--- 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
diff -r d983a020489d -r 4bc48d713602 src/Doc/ProgProve/document/intro-isabelle.tex
--- 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.