src/HOL/Isar_examples/MutilatedCheckerboard.thy
2005-11-23 wenzelm 2005-11-23 tuned induction proofs;
2005-11-16 wenzelm 2005-11-16 tuned;
2005-11-10 wenzelm 2005-11-10 tuned proofs;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2002-05-30 nipkow 2002-05-30 Modifications due to enhanced linear arithmetic.
2001-10-30 wenzelm 2001-10-30 tuned induct proofs;
2001-10-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2000-11-06 wenzelm 2000-11-06 improved: 'induct' handle non-atomic goals;
2000-11-03 wenzelm 2000-11-03 adapted "obtain" proofs;
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-08-19 wenzelm 2000-08-19 tuned;
2000-08-17 wenzelm 2000-08-17 'symmetric' attribute;
2000-08-14 wenzelm 2000-08-14 intros;
2000-07-30 wenzelm 2000-07-30 adapted obtain; tuned;
2000-05-05 wenzelm 2000-05-05 adapted to new arithmetic simprocs;
2000-04-13 nipkow 2000-04-13 Times -> <*> ** -> <*lex*>
2000-04-05 wenzelm 2000-04-05 fixed goal selection;
2000-02-24 wenzelm 2000-02-24 simplified induct method;
2000-02-22 wenzelm 2000-02-22 tuned "induct" syntax;
1999-10-28 wenzelm 1999-10-28 improved presentation;
1999-10-15 wenzelm 1999-10-15 improved presentation;
1999-10-08 wenzelm 1999-10-08 improved presentation;
1999-10-06 wenzelm 1999-10-06 improved presentation;
1999-09-21 wenzelm 1999-09-21 accomodate refined facts handling; tuned;
1999-09-04 wenzelm 1999-09-04 replaced ?? by ?;
1999-09-03 wenzelm 1999-09-03 from hyp;
1999-09-01 wenzelm 1999-09-01 tuned;
1999-08-30 wenzelm 1999-08-30 tuned;
1999-08-29 wenzelm 1999-08-29 added Isar_examples/MutilatedCheckerboard.thy;
1999-08-29 wenzelm 1999-08-29 The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;