src/HOL/Tools/record_package.ML
2008-12-05 haftmann 2008-12-05 removed Table.extend, NameSpace.extend_table
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-09-26 haftmann 2008-09-26 removed obsolete name convention "func"
2008-07-29 haftmann 2008-07-29 PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;
2008-06-19 wenzelm 2008-06-19 export read_typ/cert_typ -- version with regular context operations; tuned;
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-14 wenzelm 2008-06-14 prove_standard: more precises argument passing; proper context for tactics derived from res_inst_tac;
2008-06-10 haftmann 2008-06-10 rep_datatype command now takes list of constructors as input arguments
2008-05-18 wenzelm 2008-05-18 eliminated theory CPure;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax; removed dead code;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset;
2008-03-29 wenzelm 2008-03-29 eliminated quiete_mode ref (turned into proper argument);
2008-03-27 wenzelm 2008-03-27 removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
2008-03-20 haftmann 2008-03-20 more antiquotations
2008-02-27 schirmer 2008-02-27 removed some debugging output from trace
2008-02-17 wenzelm 2008-02-17 added get_parent (for AWE); tuned;
2008-02-13 kleing 2008-02-13 fixed record pretty printing
2007-12-19 schirmer 2007-12-19 replaced K_record by lambda term %x. c
2007-10-24 wenzelm 2007-10-24 separate RecordPackage.timing flag;
2007-10-17 wenzelm 2007-10-17 replaced NameSpace.accesses' by NameSpace.external_names (depening on naming);
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-04 wenzelm 2007-10-04 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-18 haftmann 2007-09-18 distinction between regular and default code theorems
2007-08-14 wenzelm 2007-08-14 PrimitiveDefs.mk_defpair;
2007-08-10 haftmann 2007-08-10 new structure for code generator modules
2007-07-05 wenzelm 2007-07-05 avoid polymorphic equality; removed dead code;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-20 haftmann 2007-04-20 add definitions explicitly to code generator table
2007-04-15 wenzelm 2007-04-15 adapted decode_type;
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-11 haftmann 2007-04-11 canonical merge operations
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2007-01-31 haftmann 2007-01-31 print translation for record types with empty-sorted type variables raise Match instead of producing an error
2006-12-30 wenzelm 2006-12-30 removed conditional combinator;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-11 wenzelm 2006-12-11 advanced translation functions: Proof.context;
2006-12-07 wenzelm 2006-12-07 reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 wenzelm 2006-12-07 reorganized structure Goal vs. Tactic;
2006-11-27 haftmann 2006-11-27 removed HOL structure
2006-11-14 schirmer 2006-11-14 Exported some names
2006-11-07 schirmer 2006-11-07 field-update in records is generalised to take a function on the field rather than the new value.
2006-10-31 haftmann 2006-10-31 dropped nth_update
2006-10-20 haftmann 2006-10-20 slight cleanup
2006-10-10 haftmann 2006-10-10 gen_rem(s) abandoned in favour of remove / subtract
2006-09-06 haftmann 2006-09-06 now using TypecopyPackage
2006-08-08 haftmann 2006-08-08 dropped duplicated line
2006-07-29 wenzelm 2006-07-29 Goal.prove: more tactic arguments;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-07-08 wenzelm 2006-07-08 Goal.prove: context;
2006-06-11 wenzelm 2006-06-11 avoid unqualified exception;
2006-05-30 schirmer 2006-05-30 tuned type print-translations ----------------------------------------------------------------------
2006-05-29 schirmer 2006-05-29 fixed bug in type print translations
2006-04-06 haftmann 2006-04-06 adaptions to change in typedef_package.ML
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-07 wenzelm 2006-02-07 renamed gen_duplicates to duplicates;
2006-02-06 wenzelm 2006-02-06 TableFun: renamed xxx_multi to xxx_list;