doc-src/TutorialI/fp.tex
 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 @@
\end{warn}

-\subsection{Case study: boolean expressions}
-\label{sec:boolex}
-
-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.
-
\input{Ifexpr/document/Ifexpr.tex}
-\medskip
-
-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
-\S\ref{sec:InductionHeuristics}
-
-\begin{exercise}
-  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{=}).)
-\end{exercise}

\section{Some basic types}

@@ -417,9 +395,10 @@
\begin{ttbox}\makeatother
(0#1#[]) @ []  $$\leadsto$$  0#((1#[]) @ [])  $$\leadsto$$  0#(1#([] @ []))  $$\leadsto$$  0#1#[]
\end{ttbox}
-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.

\input{Misc/document/simp.tex}

@@ -592,12 +571,4 @@

\index{induction!recursion|)}
\index{recursion induction|)}
-
\index{*recdef|)}