src/HOL/Tools/inductive_realizer.ML
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-06 wenzelm 2006-02-06 Envir.(beta_)eta_contract;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-12-06 haftmann 2005-12-06 re-oriented some result tuples in PureThy
2005-12-01 haftmann 2005-12-01 oriented pairs theory * 'a to 'a * theory
2005-10-28 haftmann 2005-10-28 swapped add_datatype result
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-09-19 haftmann 2005-09-19 introduced AList module
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-07-15 wenzelm 2005-07-15 tuned fold on terms;
2005-05-31 wenzelm 2005-05-31 Theory.restore_naming;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Args.global_const (static binding!);
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-08 berghofe 2004-06-08 add_dummies no longer uses transform_error but handles specific exception Datatype_Empty instead.
2003-04-27 berghofe 2003-04-27 Fixed problem in add_elim_realizer (concerning inductive predicates with parameters) introduced by last bugfix.
2003-04-23 berghofe 2003-04-23 Fixed problem in add_elim_realizer which caused bound variables to get mixed up.
2002-11-27 berghofe 2002-11-27 Changed format of realizers / correctness proofs.
2002-11-13 berghofe 2002-11-13 New package for constructing realizers for introduction and elimination rules of inductive predicates.