2010-08-11 ago use Pretty.enum convenience;
2010-07-23 ago observe standard conventions for doc-strings;
2010-05-30 ago replaced ML_Lex.read_antiq by more concise, which includes full read/report with explicit position information;
2010-05-27 ago renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-15 ago renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15 ago refer directly to structure Keyword and Parse;
2010-05-08 ago unified/simplified Pretty.margin_default;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-25 ago added basic reporting of test cases to quickcheck
2010-02-19 ago renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop
2009-11-08 ago adapted Theory_Data;
2009-10-29 ago standardized filter/filter_out;
2009-10-27 ago critical comments;
2009-10-25 ago eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 ago maintain theory name via name space, not tags;
2009-10-24 ago eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-10-21 ago curried union as canonical list operation
2009-10-21 ago dropped redundant gen_ prefix
2009-10-20 ago replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-19 ago Removed dead code in function mk_deftab.
2009-10-17 ago operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-17 ago indicate CRITICAL nature of various setmp combinators;
2009-10-15 ago replaced String.concat by implode;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-07-24 ago eliminated OldGoals.read_term;
2009-07-20 ago deftab: only process theorems on demand
2009-07-14 ago more accessors to unfold simpset
2009-05-14 ago merged
2009-05-14 ago quickcheck size starts with 0
2009-05-13 ago Cleaned up code of function test_term.
2009-05-12 ago transferred code generator preprocessor into separate module
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 ago Thm.add_oracle interface: replaced old bstring by binding;
2008-12-31 ago moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 ago use regular Term.add_vars, Term.add_frees etc.;
2008-12-15 ago moved value.ML to src/Tools
2008-10-23 ago renamed Thm.get_axiom_i to Thm.axiom;
2008-10-19 ago - removed test_params from CodegenData (now in Pure/Tools/quickcheck.ML)
2008-10-09 ago established canonical argument order in SML code generators
2008-09-26 ago eliminated polymorphic equality;
2008-09-22 ago generic quickcheck framework
2008-09-22 ago some steps towards generic quickcheck framework
2008-09-18 ago eval_term: CRITICAL due to eval_result;
2008-09-17 ago simplified ML_Context.eval_in -- expect immutable Proof.context value;
2008-09-16 ago generic value command
2008-08-28 ago restructured and split code serializer module
2008-08-06 ago Reverted last change, since it caused incompatibilities.
2008-08-04 ago Quoted terms in consts_code declarations are now preprocessed as well.
2008-06-30 ago simplified retrieval of theory names of consts and types
2008-06-25 ago moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-20 ago type constructors now with markup
2008-06-18 ago OldGoals.simple_read_term;
2008-05-23 ago Replaced Pretty.str and Pretty.string_of by specific functions that
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 ago cat_lines;
2008-04-17 ago Pretty.mark;
2008-04-12 ago rep_cterm/rep_thm: no longer dereference theory_ref;