src/HOL/Isar_examples/W_correct.thy
2000-11-06 wenzelm 2000-11-06 improved: 'induct' handle non-atomic goals;
2000-11-03 wenzelm 2000-11-03 adapted "obtain" proofs;
2000-10-03 wenzelm 2000-10-03 tuned;
2000-09-17 wenzelm 2000-09-17 isar-strip-terminators;
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-03-16 wenzelm 2000-03-16 Splitter support;
2000-03-13 wenzelm 2000-03-13 use cases; tuned;
2000-02-24 wenzelm 2000-02-24 simplified induct method;
2000-02-22 wenzelm 2000-02-22 tuned "induct" syntax;
2000-01-06 wenzelm 2000-01-06 obtain: renamed 'in' to 'where';
2000-01-05 wenzelm 2000-01-05 obtain;
1999-10-30 wenzelm 1999-10-30 improved presentation;
1999-10-28 wenzelm 1999-10-28 improved presentation;
1999-10-08 wenzelm 1999-10-08 tuned presentation;
1999-10-08 wenzelm 1999-10-08 improved presentation;
1999-10-06 wenzelm 1999-10-06 improved presentation;
1999-09-30 wenzelm 1999-09-30 fixed 'is' match;
1999-09-29 wenzelm 1999-09-29 lemma;
1999-09-28 wenzelm 1999-09-28 added W_correct -- correctness of Milner's type inference algorithm W (let-free version);