src/HOL/Tools/inductive_realizer.ML
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.