| Fri, 16 Mar 2012 18:20:12 +0100 | wenzelm | outer syntax command definitions based on formal command_spec derived from theory header declarations; | file | diff | annotate |
| Tue, 13 Mar 2012 20:04:24 +0100 | wenzelm | more explicit indication of def names; | file | diff | annotate |
| Mon, 27 Feb 2012 15:48:02 +0100 | wenzelm | prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required; | file | diff | annotate |
| Sat, 17 Dec 2011 13:08:03 +0100 | wenzelm | tuned signature; | file | diff | annotate |
| Sat, 17 Dec 2011 12:42:10 +0100 | wenzelm | clarified modules that contribute to datatype package; | file | diff | annotate |
| Fri, 16 Dec 2011 21:23:21 +0100 | wenzelm | eliminated old-fashioned Global_Theory.add_thms(s); | file | diff | annotate |
| Thu, 15 Dec 2011 18:08:40 +0100 | wenzelm | clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype; | file | diff | annotate |
| Thu, 15 Dec 2011 17:37:14 +0100 | wenzelm | separate rep_datatype.ML; | file | diff | annotate |