src/HOL/Isar_examples/Puzzle.thy
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2005-11-19 wenzelm 2005-11-19 tuned induct syntax;
2005-11-16 wenzelm 2005-11-16 tuned document;
2005-11-16 wenzelm 2005-11-16 improved induction proof: local defs/fixes;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2002-03-01 wenzelm 2002-03-01 tuned;
2000-11-10 wenzelm 2000-11-10 simplified induction;
2000-09-17 wenzelm 2000-09-17 isar-strip-terminators;
2000-09-12 wenzelm 2000-09-12 renamed atts: rulify to rule_format, elimify to elim_format;
2000-09-07 wenzelm 2000-09-07 updated attribute names;
2000-09-06 nipkow 2000-09-06 less_induct -> nat_less_induct
2000-05-21 wenzelm 2000-05-21 replaced {{ }} by { };
1999-11-17 wenzelm 1999-11-17 added Isar_examples/Puzzle.thy;