# HG changeset patch
# User nipkow
# Date 1373962705 -7200
# Node ID a3b04f0ab6a41b98c2b0014be38a069c61c7b9b1
# Parent  7f7311d04727c5ee8e343693c196c2763a63c275
added exercise

diff -r 7f7311d04727 -r a3b04f0ab6a4 src/Doc/ProgProve/Isar.thy
--- a/src/Doc/ProgProve/Isar.thy	Mon Jul 15 15:50:39 2013 +0200
+++ b/src/Doc/ProgProve/Isar.thy	Tue Jul 16 10:18:25 2013 +0200
@@ -590,6 +590,17 @@
 the fact just proved, in this case the preceding block. In general,
 \isacom{note} introduces a new name for one or more facts.
 
+\exercise
+Give a readable, structured proof of the following lemma:
+*}
+lemma assumes T: "\<forall> x y. T x y \<or> T y x"
+  and A: "\<forall> x y. A x y \<and> A y x \<longrightarrow> x = y"
+  and TA: "\<forall> x y. T x y \<longrightarrow> A x y" and "A x y"
+shows "T x y"
+(*<*)oops(*>*)
+text{*
+\endexercise
+
 \section{Case Analysis and Induction}
 
 \subsection{Datatype Case Analysis}