2012-02-17 wenzelm 2012-02-17 retain default of Syntax.ambiguity, according to 2bd54d4b5f3d (despite earlier versions);
2012-02-16 wenzelm 2012-02-16 simplified configuration options for syntax ambiguity;
2012-01-13 wenzelm 2012-01-13 handle specific exception, not arbitrary ones (including Interrupt);
2012-01-13 wenzelm 2012-01-13 eliminated dead code;
2011-11-24 wenzelm 2011-11-24 simplified -- empty_ss already contains minimal mksimps;
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-07-20 Cezary Kaliszyk 2011-07-20 HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.
2011-07-18 krauss 2011-07-18 killed use of PolyML.makestring
2011-07-13 Cezary Kaliszyk 2011-07-13 HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems
2011-06-09 wenzelm 2011-06-09 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext); clarified Syntax.root;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;
2011-01-10 wenzelm 2011-01-10 eliminated Int.toString;
2010-12-01 wenzelm 2010-12-01 just one Term.dest_funT;
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
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-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-09-09 wenzelm 2010-09-09 avoid handling interrupts in user code;
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2010-09-05 wenzelm 2010-09-05 turned show_brackets into proper configuration option; Sign.certify/type_check: dropped Syntax.pp_show_brackets, which is hard to hold up due to Pretty.pp and not even present in the regular end-user type check;
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-09-03 wenzelm 2010-09-03 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
2010-09-03 wenzelm 2010-09-03 turned show_all_types into proper configuration option;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-19 haftmann 2010-08-19 more antiquotations
2010-08-19 haftmann 2010-08-19 use HOLogic.boolT and @{typ bool} more pervasively
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-07-20 wenzelm 2010-07-20 discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
2010-07-12 wenzelm 2010-07-12 do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel; use up-to-date ML_Compiler.exn_message;
2010-07-01 haftmann 2010-07-01 qualified constants Set.member and Set.Collect
2010-06-11 haftmann 2010-06-11 avoid references to old constdefs
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
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-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-05-03 wenzelm 2010-05-03 minor tuning of Thm.strip_shyps -- no longer pervasive;
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-29 wenzelm 2010-04-29 proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-03-27 wenzelm 2010-03-27 separate global and local part, only the latter is transformed by morphisms;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-19 wenzelm 2010-03-19 typedef etc.: no constraints;
2010-03-13 wenzelm 2010-03-13 global typedef;
2010-02-26 wenzelm 2010-02-26 use simplified Syntax.escape;
2010-02-19 wenzelm 2010-02-19 renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-21 haftmann 2009-10-21 merged
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-10-15 wenzelm 2009-10-15 space_implode;
2009-10-15 wenzelm 2009-10-15 sort_strings (cf. Pure/library.ML);
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-08-28 wenzelm 2009-08-28 modernized messages -- eliminated ctyp/cterm operations;
2009-07-24 wenzelm 2009-07-24 ML_Context.the_local_context;