2009-07-27 ago moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-15 ago more antiquotations;
2009-06-24 ago renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-06-04 ago dropped legacy ML bindings; tuned
2009-03-26 ago simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-15 ago simplified attribute setup;
2009-03-13 ago simplified method setup;
2009-03-13 ago unified type Proof.method and pervasive METHOD combinators;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 ago removed obsolete claset_rules_of, simpset_rules_of -- as proposed in the text;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2009-03-01 ago use long names for old-style fold combinators;
2009-01-21 ago binding replaces bstring
2009-01-06 ago renamed structure ParList to Par_List;
2008-12-31 ago moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 ago moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-10 ago more antiquotations;
2008-12-04 ago cleaned up binding module and related code
2008-10-23 ago renamed Thm.get_axiom_i to Thm.axiom;
2008-10-09 ago improved performance of skolem cache, due to parallel map;
2008-09-17 ago back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-09-03 ago Sign.declare_const: Name.binding;
2008-08-14 ago moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-09 ago unified Args.T with OuterLex.token, renamed some operations;
2008-06-23 ago Logic.all/mk_equals/mk_implies;
2008-06-13 ago skolem_fact/thm: uniform numbering, even for singleton list;
2008-06-12 ago use regular error function;
2008-06-12 ago export just one setup function;
2008-06-12 ago ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
2008-06-12 ago declare_skofuns/skolem: canonical argument order;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 ago structure Display: less pervasive operations;
2008-04-15 ago Thm.forall_elim_var(s);
2008-04-12 ago rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-10 ago tuned;
2008-04-07 ago * Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
2008-01-02 ago testing for empty sort
2007-10-31 ago Catch exceptions arising during the abstraction operation.
2007-10-30 ago bugfixes concerning strange theorems
2007-10-12 ago trying to make it run faster
2007-10-11 ago replaced Sign.add_consts_authentic by Sign.declare_const;
2007-10-09 ago context-based treatment of generalization; also handling TFrees in axiom clauses
2007-10-05 ago filtering out some package theorems
2007-10-04 ago combinator translation
2007-10-03 ago skolem_cache: ignore internal theorems -- major speedup;
2007-09-30 ago llabs/sko: removed Name.internal;
2007-09-30 ago skofuns/absfuns: explicit markup as internal consts;
2007-09-27 ago removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
2007-09-21 ago proper signature constraint;
2007-09-18 ago metis now available in PreList
2007-08-17 ago proper signature for Meson;
2007-08-10 ago removal of some refs
2007-08-03 ago replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-07-29 ago simplified ResAtpset via NamedThmsFun;
2007-07-05 ago renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-06-13 ago renamed Goal.prove_raw to Goal.prove_internal;
2007-05-10 ago moved some Drule operations to Thm (see more_thm.ML);
2007-05-07 ago simplified DataFun interfaces;
2007-04-19 ago trying to make single-step proofs work better, especially if they contain