2010-08-11 wenzelm 2010-08-11 use Pretty.enum convenience;
2010-07-23 wenzelm 2010-07-23 observe standard conventions for doc-strings;
2010-05-30 wenzelm 2010-05-30 replaced ML_Lex.read_antiq by more concise, which includes full read/report with explicit position information; ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information; fall back on ML_Context.eval_text if there is no position or no surrounding text; proper Args.name_source_position for method "tactic" and "raw_tactic"; tuned;
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-15 wenzelm 2010-05-15 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-05-08 wenzelm 2010-05-08 unified/simplified Pretty.margin_default; discontinued special Pretty.setmargin etc; explicit margin argument for Pretty.string_of_margin etc.;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
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-02-25 bulwahn 2010-02-25 added basic reporting of test cases to quickcheck
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-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-27 wenzelm 2009-10-27 critical comments;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 wenzelm 2009-10-25 maintain theory name via name space, not tags; AxClass.thynames_of_arity: explicit theory name, not tags;
2009-10-24 wenzelm 2009-10-24 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-10-21 haftmann 2009-10-21 curried union as canonical list operation
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-19 berghofe 2009-10-19 Removed dead code in function mk_deftab.
2009-10-17 wenzelm 2009-10-17 operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-24 wenzelm 2009-07-24 eliminated OldGoals.read_term;
2009-07-20 haftmann 2009-07-20 deftab: only process theorems on demand
2009-07-14 haftmann 2009-07-14 more accessors to unfold simpset
2009-05-14 haftmann 2009-05-14 merged
2009-05-14 haftmann 2009-05-14 quickcheck size starts with 0
2009-05-13 berghofe 2009-05-13 Cleaned up code of function test_term.
2009-05-12 haftmann 2009-05-12 transferred code generator preprocessor into separate module
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 Thm.add_oracle interface: replaced old bstring by binding;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 use regular Term.add_vars, Term.add_frees etc.; moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-15 haftmann 2008-12-15 moved value.ML to src/Tools
2008-10-23 wenzelm 2008-10-23 renamed Thm.get_axiom_i to Thm.axiom;
2008-10-19 berghofe 2008-10-19 - removed test_params from CodegenData (now in Pure/Tools/quickcheck.ML) - improved code unfold preprocessor: now uses one single simpset containing all unfolding rules - got rid of some legacy functions
2008-10-09 haftmann 2008-10-09 established canonical argument order in SML code generators
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-09-22 haftmann 2008-09-22 generic quickcheck framework
2008-09-22 haftmann 2008-09-22 some steps towards generic quickcheck framework
2008-09-18 wenzelm 2008-09-18 eval_term: CRITICAL due to eval_result; simplified oracle interface;
2008-09-17 wenzelm 2008-09-17 simplified ML_Context.eval_in -- expect immutable Proof.context value; parse_code: operate on thy, which contains the ML environment;
2008-09-16 haftmann 2008-09-16 generic value command
2008-08-28 haftmann 2008-08-28 restructured and split code serializer module
2008-08-06 berghofe 2008-08-06 Reverted last change, since it caused incompatibilities.
2008-08-04 berghofe 2008-08-04 Quoted terms in consts_code declarations are now preprocessed as well.
2008-06-30 haftmann 2008-06-30 simplified retrieval of theory names of consts and types
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-20 haftmann 2008-06-20 type constructors now with markup
2008-06-18 wenzelm 2008-06-18 OldGoals.simple_read_term;
2008-05-23 berghofe 2008-05-23 Replaced Pretty.str and Pretty.string_of by specific functions that set print_mode and margin appropriately.
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 cat_lines;
2008-04-17 wenzelm 2008-04-17 Pretty.mark;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;