# HG changeset patch
# User nipkow
# Date 1383411028 -3600
# Node ID e039a9b9700def80c11ef3b8759d222a05152847
# Parent  2975658d49cd1395ba94c015ef8d357813c826e3
more exercises

diff -r 2975658d49cd -r e039a9b9700d src/Doc/ProgProve/Isar.thy
--- a/src/Doc/ProgProve/Isar.thy	Sat Nov 02 17:19:34 2013 +0100
+++ b/src/Doc/ProgProve/Isar.thy	Sat Nov 02 17:50:28 2013 +0100
@@ -1079,9 +1079,21 @@
 
 \subsection{Exercises}
 
+
+\exercise
+Give a structured proof of @{prop "ev(Suc(Suc n)) \<Longrightarrow> ev n"}
+by rule inversion:
+*}
+
+lemma assumes a: "ev(Suc(Suc n))" shows "ev n"
+(*<*)oops(*>*)
+
+text{*
+\endexercise
+
 \begin{exercise}
-Give a structured proof of @{prop "\<not> ev(Suc(Suc(Suc 0)))"}.
-Rule inversion is sufficient. If there are no cases to be proved you can close
+Give a structured proof of @{prop "\<not> ev(Suc(Suc(Suc 0)))"}
+by rule inversions. If there are no cases to be proved you can close
 a proof immediateley with \isacom{qed}.
 \end{exercise}