# HG changeset patch
# User nipkow
# Date 985968746 -7200
# Node ID 17403c5a9eb19093f64ed0fafba932f4c97f3674
# Parent  860c65c7388a0e3710d1a6c3dcc7d075f52aa301
*** empty log message ***

diff -r 860c65c7388a -r 17403c5a9eb1 doc-src/TutorialI/Overview/FP1.thy
--- a/doc-src/TutorialI/Overview/FP1.thy	Fri Mar 30 16:12:57 2001 +0200
+++ b/doc-src/TutorialI/Overview/FP1.thy	Fri Mar 30 18:12:26 2001 +0200
@@ -141,11 +141,9 @@
 
 subsubsection{*Tracing*}
 
-ML "set trace_simp"
 lemma "rev [a] = []"
 apply(simp)
 oops
-ML "reset trace_simp"
 
 
 
@@ -193,22 +191,9 @@
 theorem "exec (comp e) s [] = [value e s]";
 oops
 
-theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
-oops
-
-lemma exec_app[simp]:
-  "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
-apply(induct_tac xs)
-apply(simp)
-apply(simp split: instr.split)
-done
-
-theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
-by(induct_tac e, auto)
 
 
-
-subsection{*Advanced Datatupes*}
+subsection{*Advanced Datatypes*}
 
 
 subsubsection{*Mutual Recursion*}
@@ -279,8 +264,11 @@
 apply simp_all
 oops
 
-lemma "mirrors ts = rev(map mirror ts)"
-by(induct ts, simp_all)
+text{*
+\begin{exercise}
+Complete the above proof.
+\end{exercise}
+*}
 
 
 subsubsection{*Datatypes Involving Functions*}
@@ -303,4 +291,10 @@
 datatype lambda = C "lambda \<Rightarrow> lambda"
 *)
 
+text{*
+\begin{exercise}
+Define a datatype of ordinals and the ordinal Gamma0.
+\end{exercise}
+*}
+
 end
diff -r 860c65c7388a -r 17403c5a9eb1 doc-src/TutorialI/Overview/RECDEF.thy
--- a/doc-src/TutorialI/Overview/RECDEF.thy	Fri Mar 30 16:12:57 2001 +0200
+++ b/doc-src/TutorialI/Overview/RECDEF.thy	Fri Mar 30 18:12:26 2001 +0200
@@ -75,4 +75,11 @@
 apply(simp add:rev_map sym[OF map_compose] cong:map_cong)
 done
 
+text{*
+\begin{exercise}
+Define a function for merging two ordered lists (of natural numbers) and
+show that if the two input lists are ordered, so is the output.
+\end{exercise}
+*}
+
 end
diff -r 860c65c7388a -r 17403c5a9eb1 doc-src/TutorialI/Overview/document/session.tex
--- a/doc-src/TutorialI/Overview/document/session.tex	Fri Mar 30 16:12:57 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-\input{FP0.tex}
-
-\input{FP1.tex}
-
-\input{RECDEF.tex}
-
-\input{Rules.tex}
-
-\input{Sets.tex}
-
-\input{Ind.tex}
-
-\input{Isar.tex}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: