src/HOL/Tools/Datatype/datatype_rep_proofs.ML
2009-09-27 haftmann 2009-09-27 registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
2009-07-21 haftmann 2009-07-21 dropped ancient flat_names option
2009-07-10 haftmann 2009-07-10 dropped find_index_eq
2009-07-06 haftmann 2009-07-06 moved Inductive.myinv to Fun.inv; tuned
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories