2011-11-07 ago tuned signature -- avoid spurious Thm.mixed_attribute;
2011-11-03 ago tuned signature -- canonical argument order;
2011-08-13 ago less verbosity in batch mode -- spam reduction and notable performance improvement;
2011-06-09 ago tuned signature: Name.invent and Name.invent_names;
2011-04-27 ago tuned signature -- eliminated odd comment;
2011-04-27 ago more uniform Variable.add_frees/add_fixed etc.;
2011-04-21 ago discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago tuned signature, disentangled dependencies;
2011-04-06 ago parallel parsing of big specifications;
2011-03-24 ago added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2011-01-08 ago misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-12 ago eliminated aliases of Type.constraint;
2010-08-12 ago Named_Target.theory_init
2010-08-11 ago renamed Theory_Target to the more appropriate Named_Target
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-27 ago renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-29 ago ProofContext.read_const: allow for type constraint (for fixed variable);
2010-04-25 ago modernized naming conventions of main Isar proof elements;
2010-04-23 ago explicit 'schematic_theorem' etc. for schematic theorem statements;
2010-04-11 ago Thm.add_axiom/add_def: return internal name of foundational axiom;
2010-03-22 ago added Specification.axiom convenience;
2010-03-07 ago modernized structure Object_Logic;
2010-03-07 ago modernized structure Local_Defs;
2010-03-01 ago added type_notation command;
2010-02-27 ago clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
2009-11-19 ago Specification.definition: Thm.definitionK marks exactly the high-level end-user result;
2009-11-19 ago replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
2009-11-15 ago axiomatization: declare Spec_Rules, direct result;
2009-11-13 ago modernized structure Local_Theory;
2009-11-13 ago eliminated slightly odd kind argument of LocalTheory.note(s);
2009-11-12 ago eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-11-05 ago declare Spec_Rules for most basic definitional packages;
2009-11-02 ago modernized structure Proof_Display;
2009-11-02 ago modernized structure AutoBind;
2009-11-01 ago modernized structure Context_Rules;
2009-11-01 ago modernized structure Rule_Cases;
2009-10-25 ago eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-02 ago clarified Proof.refine_insert -- always "refine" to apply standard method treatment (of conjunctions);
2009-09-30 ago eliminated dead code;
2009-09-23 ago handling of definitions
2009-09-23 ago experimenting to add some useful interface for definitions
2009-03-28 ago renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 ago renamed ProofContext.note_thmss_i to ProofContext.note_thmss, 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 simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
2009-03-12 ago Assumption.local_prems_of;
2009-03-12 ago axiomatization: more precise treatment of binding;
2009-03-11 ago Thm.def_binding_optional;
2009-03-07 ago more uniform handling of binding in targets and derived elements;
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-01-21 ago removed Ids;
2009-01-21 ago binding is alias for Binding.T
2008-12-19 ago All logics ported to new locales.
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code