2013-01-22 traytel 2013-01-22 separate data used for case translation from the datatype package
2013-01-22 berghofe 2013-01-22 case translations performed in a separate check phase (with adjustments by traytel)
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
2012-09-05 wenzelm 2012-09-05 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
2012-08-30 blanchet 2012-08-30 more work on BNF sugar -- up to derivation of nchotomy
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-13 wenzelm 2012-03-13 more explicit indication of def names;
2012-02-27 wenzelm 2012-02-27 prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
2011-12-17 wenzelm 2011-12-17 tuned signature;
2011-12-17 wenzelm 2011-12-17 clarified modules that contribute to datatype package;
2011-12-16 wenzelm 2011-12-16 eliminated old-fashioned Global_Theory.add_thms(s);
2011-12-15 wenzelm 2011-12-15 clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
2011-12-15 wenzelm 2011-12-15 separate rep_datatype.ML; tuned signature;