src/HOL/Tools/record.ML
2011-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-04-06 wenzelm 2011-04-06 typed_print_translation: discontinued show_sorts argument;
2011-04-06 wenzelm 2011-04-06 moved unparse material to syntax_phases.ML;
2011-04-06 wenzelm 2011-04-06 renamed Standard_Syntax to Syntax_Phases;
2011-04-05 wenzelm 2011-04-05 moved decode/parse operations to standard_syntax.ML; tuned;
2011-03-26 wenzelm 2011-03-26 added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent; recovered printing of Hoare assign statements from 45d090186bbe;
2011-03-11 bulwahn 2011-03-11 adaptions in generators using the common functions
2011-03-11 bulwahn 2011-03-11 adapting record package to renaming of quickcheck's structures
2011-01-16 wenzelm 2011-01-16 proper type variables with sorts;
2011-01-15 wenzelm 2011-01-15 recovered printing of record updates over compound terms, e.g. "(|x = a|)(|x := b|)", which was apparently broken in 45a2ffc5911e; tuned;
2011-01-15 wenzelm 2011-01-15 export Record.get_hierarchy -- external tools typically need this information;
2011-01-15 wenzelm 2011-01-15 tuned;
2011-01-15 wenzelm 2011-01-15 removed unreferenced identifiers;
2011-01-10 wenzelm 2011-01-10 standardized split_last/last_elem towards List.last; eliminated obsolete Library.last_elem;
2010-12-01 wenzelm 2010-12-01 just one HOLogic.mk_comp;
2010-12-01 wenzelm 2010-12-01 more direct use of binder_types/body_type;
2010-12-01 wenzelm 2010-12-01 just one Term.dest_funT;
2010-11-26 wenzelm 2010-11-26 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-11-03 wenzelm 2010-11-03 try_param_tac: plain user error appears more appropriate;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-26 wenzelm 2010-08-26 misc tuning and simplification, notably theory data;
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-18 haftmann 2010-08-18 re-added instantiation of type class random for records
2010-08-17 haftmann 2010-08-17 tuned code
2010-08-17 haftmann 2010-08-17 use extension constant as formal constructor of logical record type
2010-08-17 haftmann 2010-08-17 authentic syntax allows simplification of type names
2010-08-17 haftmann 2010-08-17 dropped make_/dest_ naming convention
2010-08-17 haftmann 2010-08-17 formally integrated typecopy layer into record package
2010-08-13 haftmann 2010-08-13 avoid variable name acc (cf. cs. 3142c1e21a0e)
2010-08-09 wenzelm 2010-08-09 tuned comments;
2010-07-27 haftmann 2010-07-27 delete structure Basic_Record; avoid `record` in names in structure Record
2010-07-12 wenzelm 2010-07-12 moved misc legacy stuff from OldGoals to Misc_Legacy; OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;
2010-06-19 haftmann 2010-06-19 more binding; avoid arcane Rep and Abs prefixes
2010-06-19 haftmann 2010-06-19 cleanup of typecopy package
2010-05-29 wenzelm 2010-05-29 explicit markup for forked goals, as indicated by Goal.fork; accumulate pending forks within command state and hilight accordingly; Isabelle_Process: enforce future_terminal_proof, which gives some impression of non-linear/parallel checking;
2010-05-26 haftmann 2010-05-26 dropped legacy theorem bindings
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-16 wenzelm 2010-04-16 modernized type abbreviations;
2010-04-15 wenzelm 2010-04-15 more robust record syntax: use Type.raw_match to ignore sort constraints as in regular abbreviations (also note that constraints only affect operations, not types);
2010-04-15 wenzelm 2010-04-15 replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo; simplified via ProofContext.check_tfree;
2010-04-15 wenzelm 2010-04-15 modernized treatment of sort constraints in specification; pass-through type variables as usual as (string * sort) internally -- recovers proper sort handling;
2010-04-14 krauss 2010-04-14 record package: corrected sort handling in type translations to avoid crashes when default sort is changed. Test case: record 'a T = elem :: 'a defaultsort order term elem (* low-level exception *)
2010-03-27 wenzelm 2010-03-27 Typedef.info: separate global and local part, only the latter is transformed by morphisms;
2010-03-27 wenzelm 2010-03-27 moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
2010-03-13 wenzelm 2010-03-13 global typedef;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-06 wenzelm 2010-03-06 record_type_tr': more robust strip_fields (printed types are not necessarily well-formed, e.g. in Syntax.pretty_arity);
2010-03-06 wenzelm 2010-03-06 record_type_abbr_tr': removed obsolete workaround for decode_type, which now retains syntactic categories of variables vs. constructors (authentic syntax);
2010-03-03 wenzelm 2010-03-03 adapted to authentic syntax -- actual types are verbatim;
2010-02-28 wenzelm 2010-02-28 more antiquotations;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2010-02-25 wenzelm 2010-02-25 explicit @{type_syntax} markup;