2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2010-03-04 wenzelm 2010-03-04 renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort; metis: type_has_topsort leads to tactic failure (with warning), like other metis failures;
2009-11-21 wenzelm 2009-11-21 explicitly mark some legacy freeze operations;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 modernized some structure names;
2009-10-29 wenzelm 2009-10-29 proper header;
2009-10-29 wenzelm 2009-10-29 replaced slightly odd Thm.is_internal by Facts.is_concealed -- as provided by the name space; tuned;
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 conceal consts via name space, not tags;
2009-10-21 haftmann 2009-10-21 merged
2009-10-21 haftmann 2009-10-21 curried union as canonical list operation
2009-10-21 haftmann 2009-10-21 removed old-style \ and \\ infixes
2009-10-21 haftmann 2009-10-21 merged
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 wenzelm 2009-10-20 modernized session Metis_Examples;
2009-10-20 paulson 2009-10-20 Removal of the unused atpset concept, the atp attribute and some related code.
2009-10-18 wenzelm 2009-10-18 removed some unreferenced material; tuned;
2009-10-16 wenzelm 2009-10-16 local channels for tracing/debugging;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-30 wenzelm 2009-07-30 qualified Subgoal.FOCUS;
2009-07-29 wenzelm 2009-07-29 Meson.first_order_resolve: avoid handle _; proper context for various Meson and Metis rules and tactics unified meson_tac/meson_claset_tac;
2009-07-28 wenzelm 2009-07-28 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS; external_prover: neg_conjecture_clauses should handle TVars within goals; misc tuning;
2009-07-27 wenzelm 2009-07-27 moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-06-24 wenzelm 2009-06-24 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again);
2009-06-04 haftmann 2009-06-04 dropped legacy ML bindings; tuned
2009-03-26 wenzelm 2009-03-26 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 wenzelm 2009-03-15 simplified attribute setup;
2009-03-13 wenzelm 2009-03-13 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
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 removed obsolete claset_rules_of, simpset_rules_of -- as proposed in the text;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2009-01-06 wenzelm 2009-01-06 renamed structure ParList to Par_List;
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 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-10 wenzelm 2008-12-10 more antiquotations;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-10-23 wenzelm 2008-10-23 renamed Thm.get_axiom_i to Thm.axiom;
2008-10-09 wenzelm 2008-10-09 improved performance of skolem cache, due to parallel map; misc tuning, less verbosity;
2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-09-03 wenzelm 2008-09-03 Sign.declare_const: Name.binding;
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;
2008-06-13 wenzelm 2008-06-13 skolem_fact/thm: uniform numbering, even for singleton list; declare_skofuns: eliminated recovery via Clausify_failure -- should be sufficiently robust as is;
2008-06-12 wenzelm 2008-06-12 use regular error function;
2008-06-12 wenzelm 2008-06-12 export just one setup function; more antiquotations; to_nnf: import open, avoiding internal variables (bounds); ThmCache: added table of seen fact names; reorganized skolem_thm/skolem_fact/saturate_skolem_cache: maintain seen fact names, ensure idempotent operation for Theory.at_end; removed obsolete skolem attribute (NB: official fact name unavailable here);
2008-06-12 wenzelm 2008-06-12 ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context; eliminated obscure theory merge/transfer -- use explicit theory context instead;
2008-06-12 wenzelm 2008-06-12 declare_skofuns/skolem: canonical argument order; minor tuning;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-15 wenzelm 2008-04-15 Thm.forall_elim_var(s);
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref; replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);