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