src/HOL/ex/InductiveInvariant_examples.thy
2006-06-05 krauss 2006-06-05 Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure". This simplifies some proofs.
2006-05-12 nipkow 2006-05-12 added lemma in_measure
2005-09-14 wenzelm 2005-09-14 tuned headers etc.;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-03-30 paulson 2005-03-30 converted from DOS to UNIX format
2003-10-22 paulson 2003-10-22 InductiveInvariant_examples illustrates advanced recursive function definitions