CookBook/Package/Ind_Examples.thy
changeset 124 0b9fa606a746
parent 120 c39f83d8daeb
--- a/CookBook/Package/Ind_Examples.thy	Tue Feb 17 13:53:54 2009 +0000
+++ b/CookBook/Package/Ind_Examples.thy	Wed Feb 18 17:17:37 2009 +0000
@@ -306,6 +306,8 @@
 qed
 
 text {*
+  (FIXME check that the code works like as indicated)
+
   The point of these examples is to get a feeling what the automatic proofs 
   should do in order to solve all inductive definitions we throw at them. For this 
   it is instructive to look at the general construction principle