src/Pure/Isar/specification.ML
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2010-03-01 wenzelm 2010-03-01 added type_notation command;
2010-02-27 wenzelm 2010-02-27 clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
2009-11-19 wenzelm 2009-11-19 Specification.definition: Thm.definitionK marks exactly the high-level end-user result;
2009-11-19 bulwahn 2009-11-19 replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
2009-11-15 wenzelm 2009-11-15 axiomatization: declare Spec_Rules, direct result;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-13 wenzelm 2009-11-13 eliminated slightly odd kind argument of LocalTheory.note(s); added LocalTheory.notes_kind as fall-back for unusual cases;
2009-11-12 wenzelm 2009-11-12 eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-05 wenzelm 2009-11-05 declare Spec_Rules for most basic definitional packages;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Display;
2009-11-02 wenzelm 2009-11-02 modernized structure AutoBind;
2009-11-01 wenzelm 2009-11-01 modernized structure Context_Rules;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-02 wenzelm 2009-10-02 clarified Proof.refine_insert -- always "refine" to apply standard method treatment (of conjunctions);
2009-09-30 wenzelm 2009-09-30 eliminated dead code;
2009-09-23 bulwahn 2009-09-23 handling of definitions
2009-09-23 bulwahn 2009-09-23 experimenting to add some useful interface for definitions
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-19 wenzelm 2009-03-19 use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-12 wenzelm 2009-03-12 simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements; simplified check_specification, read_specification: operate on a single list of simultaneous statements; tuned;
2009-03-12 wenzelm 2009-03-12 Assumption.local_prems_of;
2009-03-12 wenzelm 2009-03-12 axiomatization: more precise treatment of binding;
2009-03-11 wenzelm 2009-03-11 Thm.def_binding_optional;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in targets and derived elements;
2009-03-03 wenzelm 2009-03-03 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; minor tuning;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-19 ballarin 2008-12-19 All logics ported to new locales.
2008-12-05 haftmann 2008-12-05 Name.name_of -> Binding.base_name
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-12-01 haftmann 2008-12-01 new Binding module
2008-11-24 ballarin 2008-11-24 Enable switching to new locales during session.
2008-11-24 ballarin 2008-11-24 More ramifications of removal of 'includes' element.
2008-11-20 haftmann 2008-11-20 tuned name bindings
2008-11-20 wenzelm 2008-11-20 removed traces of former 'includes' element;
2008-11-17 haftmann 2008-11-17 adjusted locale signature to *_cmd convention
2008-11-14 haftmann 2008-11-14 Name.is_nothing
2008-10-30 ballarin 2008-10-30 Dropped context element 'includes'.
2008-10-28 haftmann 2008-10-28 cleanup code default attribute
2008-09-26 haftmann 2008-09-26 removed obsolete name convention "func"
2008-09-03 wenzelm 2008-09-03 axiomatization is now global-only;
2008-09-02 wenzelm 2008-09-02 ProofDisplay.print_results;
2008-09-02 wenzelm 2008-09-02 type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements; simplified ProofContext.inferred_param;
2008-08-13 wenzelm 2008-08-13 ProofDisplay.theory_results;
2008-04-09 wenzelm 2008-04-09 print_consts only for external specifications;
2008-03-20 wenzelm 2008-03-20 renamed former get_thms(_silent) to get_fact(_silent);
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2007-11-10 wenzelm 2007-11-10 notation: improved ProofContext.read_const does the job;
2007-10-26 wenzelm 2007-10-26 notation: associate syntax to checked-unchecked term;
2007-10-13 wenzelm 2007-10-13 renamed LocalTheory.def to LocalTheory.define;
2007-10-12 wenzelm 2007-10-12 more informative TheoryTarget.peek operation;
2007-10-11 wenzelm 2007-10-11 removed unused/impure quiet_mode; local_theory: incorporated consts into axioms; tuned;
2007-10-10 wenzelm 2007-10-10 generalized notation interface (add or del);
2007-10-09 wenzelm 2007-10-09 Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;