src/Pure/Isar/specification.ML
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
2008-12-01 ago new Binding module
2008-11-24 ago Enable switching to new locales during session.
2008-11-24 ago More ramifications of removal of 'includes' element.
2008-11-20 ago tuned name bindings
2008-11-20 ago removed traces of former 'includes' element;
2008-11-17 ago adjusted locale signature to *_cmd convention
2008-11-14 ago Name.is_nothing
2008-10-30 ago Dropped context element 'includes'.
2008-10-28 ago cleanup code default attribute
2008-09-26 ago removed obsolete name convention "func"
2008-09-03 ago axiomatization is now global-only;
2008-09-02 ago ProofDisplay.print_results;
2008-09-02 ago type Attrib.binding abbreviates Name.binding without attributes;
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-08-13 ago ProofDisplay.theory_results;
2008-04-09 ago print_consts only for external specifications;
2008-03-20 ago renamed former get_thms(_silent) to get_fact(_silent);