2010-03-13 ago Local_Defs.contract convenience;
2010-03-11 ago more basic Local_Defs.export_cterm;
2010-03-07 ago modernized structure Local_Defs;
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-11-02 ago modernized structure Primitive_Defs;
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-06-24 ago renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-03-28 ago renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-19 ago use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-12 ago Assumption.all_prems_of, Assumption.all_assms_of;
2009-03-11 ago Thm.def_binding_optional;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
2009-03-03 ago Thm.binding;
2009-01-21 ago binding is alias for Binding.T
2009-01-11 ago stripped Id
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-03-27 ago eliminated theory ProtoPure;
2007-10-20 ago added fixed_abbrev;
2007-10-19 ago tuned interfaces;
2007-10-14 ago added add_def;
2007-10-11 ago added export_cterm;
2007-10-11 ago dest/cert_def: replaced Pretty.pp by explicit Proof.context;
2007-10-11 ago moved ProofContext.pp to Syntax.pp;
2007-08-14 ago PrimitiveDefs.dest/abs_def;
2007-07-29 ago renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-07-03 ago exported meta_rewrite_conv;
2007-05-10 ago moved conversions to structure Conv;
2007-05-07 ago simplified DataFun interfaces;
2007-04-15 ago Thm.fold_terms;
2007-04-14 ago tuned signature;
2007-04-03 ago renamed Variable.import to import_thms (avoid clash with Alice keywords);
2006-12-14 ago added trans_terms/props;
2006-12-12 ago tuned expand_term;
2006-12-07 ago reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 ago expand_term: based on Envir.expand_term;
2006-12-07 ago reorganized structure Goal vs. Tactic;
2006-12-06 ago added expand;
2006-11-29 ago added export;
2006-11-28 ago simplified '?' operator;
2006-11-23 ago prefer Proof.context over Context.generic;
2006-10-11 ago add_defs: declare terms;
2006-10-09 ago simplified derived_def;
2006-10-07 ago replaced add_def by more elaborate add_defs;
2006-08-02 ago normalized Proof.context/method type aliases;
2006-07-27 ago moved basic assumption operations from structure ProofContext to Assumption;
2006-07-08 ago Goal.prove: context;
2006-07-06 ago def_export: Drule.generalize;
2006-06-15 ago ProofContext: moved variable operations to struct Variable;
2006-05-07 ago removed 'concl is' patterns;
2006-02-06 ago cert_def: use Logic.dest_def;
2006-02-02 ago tuned comments;
2006-01-31 ago (un)fold: no raw flag;
2006-01-31 ago export meta_rewrite_rule;
2006-01-29 ago added attributes defn_add/del;
2006-01-28 ago Basic operations on local definitions.
2001-10-16 ago simplified exporter interface;