changeset 9933 9feb1e0c4cb3
parent 9844 8016321c7de1
child 10181 c07860c826c5
--- a/doc-src/TutorialI/fp.tex	Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/fp.tex	Tue Sep 12 15:43:15 2000 +0200
@@ -225,29 +225,7 @@
-\subsection{Case study: boolean expressions}
-The aim of this case study is twofold: it shows how to model boolean
-expressions and some algorithms for manipulating them, and it demonstrates
-the constructs introduced above.
-How does one come up with the required lemmas? Try to prove the main theorems
-without them and study carefully what \isa{auto} leaves unproved. This has
-to provide the clue.  The necessity of universal quantification
-(\isa{\isasymforall{}t e}) in the two lemmas is explained in
-  We strengthen the definition of a \isa{normal} If-expression as follows:
-  the first argument of all \isa{IF}s must be a variable. Adapt the above
-  development to this changed requirement. (Hint: you may need to formulate
-  some of the goals as implications (\isasymimp) rather than equalities
-  (\isa{=}).)
 \section{Some basic types}
@@ -417,9 +395,10 @@
 (0#1#[]) @ []  \(\leadsto\)  0#((1#[]) @ [])  \(\leadsto\)  0#(1#([] @ []))  \(\leadsto\)  0#1#[]
-This is also known as \bfindex{term rewriting} and the equations are referred
-to as \bfindex{rewrite rules}. ``Rewriting'' is more honest than ``simplification''
-because the terms do not necessarily become simpler in the process.
+This is also known as \bfindex{term rewriting}\indexbold{rewriting} and the
+equations are referred to as \textbf{rewrite rules}\indexbold{rewrite rule}.
+``Rewriting'' is more honest than ``simplification'' because the terms do not
+necessarily become simpler in the process.
@@ -592,12 +571,4 @@
 \index{recursion induction|)}
-\subsection{Advanced forms of recursion}