src/HOL/Isar_examples/ExprCompiler.thy
2005-11-16 wenzelm 2005-11-16 tuned document;
2005-11-10 wenzelm 2005-11-10 tuned proofs;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2002-08-27 wenzelm 2002-08-27 avoid duplicate fact bindings;
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2001-10-16 wenzelm 2001-10-16 tuned induction proofs;
2000-09-17 wenzelm 2000-09-17 isar-strip-terminators;
2000-08-19 wenzelm 2000-08-19 tuned;
2000-02-27 wenzelm 2000-02-27 even better induct setup;
2000-02-22 wenzelm 2000-02-22 tuned "induct" syntax;
1999-12-07 wenzelm 1999-12-07 tuned;
1999-12-07 wenzelm 1999-12-07 tuned;
1999-11-24 wenzelm 1999-11-24 renamed comp to compile (avoids clash with Relation.comp);
1999-10-30 wenzelm 1999-10-30 improved presentation;
1999-10-15 wenzelm 1999-10-15 improved presentation;
1999-10-14 wenzelm 1999-10-14 improved presentation;
1999-10-06 wenzelm 1999-10-06 improved presentation;
1999-10-06 wenzelm 1999-10-06 improved presentation;
1999-10-05 wenzelm 1999-10-05 tuned comments;
1999-09-21 wenzelm 1999-09-21 accomodate refined facts handling; tuned;
1999-09-04 wenzelm 1999-09-04 replaced ?? by ?;
1999-08-18 wenzelm 1999-08-18 tuned;
1999-07-08 wenzelm 1999-07-08 tuned indentation;
1999-06-05 wenzelm 1999-06-05 tuned comments;
1999-05-28 wenzelm 1999-05-28 tuned formal comments;
1999-05-27 wenzelm 1999-05-27 changed {| |} verbatim syntax to {* *};
1999-04-27 wenzelm 1999-04-27 tuned;
1999-04-23 wenzelm 1999-04-23 tuned antiquotations;
1999-04-22 wenzelm 1999-04-22 tuned;
1999-04-16 wenzelm 1999-04-16 Miscellaneous Isabelle/Isar examples for Higher-Order Logic.