src/Pure/Isar/locale.ML
2008-12-05 haftmann 2008-12-05 removed Table.extend, NameSpace.extend_table
2008-12-05 haftmann 2008-12-05 dropped NameSpace.declare_base
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-12-03 ballarin 2008-12-03 Made global_note_qualified public.
2008-12-01 haftmann 2008-12-01 new Binding module
2008-12-01 haftmann 2008-12-01 Locale.*note* with conventional argument type
2008-12-01 ballarin 2008-12-01 Methods intro_locales and unfold_locales apply to both old and new locales.
2008-11-27 ballarin 2008-11-27 Fixed strange indentation.
2008-11-20 haftmann 2008-11-20 Locale.local_note_qualified
2008-11-20 haftmann 2008-11-20 tuned name bindings
2008-11-17 haftmann 2008-11-17 explicit name morphism function for locale interpretation
2008-11-14 ballarin 2008-11-14 Made local_note_prefix public.
2008-11-14 haftmann 2008-11-14 namify and name_decl combinators
2008-11-13 haftmann 2008-11-13 proper name morphisms for locales
2008-11-10 haftmann 2008-11-10 restruced naming code in anticipation of introduction of name morphisms
2008-11-10 haftmann 2008-11-10 using explicit interpretaton prefix in Name.binding (still on the surface)
2008-10-30 ballarin 2008-10-30 Dropped context element 'includes'.
2008-10-27 ballarin 2008-10-27 Extension of interface: declarations_of.
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-09-17 ballarin 2008-09-17 Public interface to interpretation morphism.
2008-09-16 ballarin 2008-09-16 Clearer separation of interpretation frontend and backend.
2008-09-03 wenzelm 2008-09-03 Sign.declare_const: Name.binding;
2008-09-03 wenzelm 2008-09-03 Name.qualified;
2008-09-02 ballarin 2008-09-02 Interpretation commands no longer accept interpretation attributes.
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;
2008-08-28 haftmann 2008-08-28 no parameter prefix for class interpretation
2008-08-27 ballarin 2008-08-27 Consistent naming of theorems in interpretation.
2008-08-27 wenzelm 2008-08-27 get rid of tabs;
2008-08-26 ballarin 2008-08-26 Reorganisation of registration code.
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-06 ballarin 2008-08-06 Interpretation command (theory/proof context) no longer simplifies goal.
2008-08-01 ballarin 2008-08-01 Removed import and lparams from locale record.
2008-07-30 haftmann 2008-07-30 facts_of
2008-07-29 haftmann 2008-07-29 tuned; explicit export of element accessors
2008-07-26 haftmann 2008-07-26 tuned function name
2008-07-25 haftmann 2008-07-25 dropped locale (open)
2008-05-18 wenzelm 2008-05-18 Syntax.string_of_typ: proper context;
2008-04-14 ballarin 2008-04-14 Changed naming scheme for theorems generated by interpretations.
2008-04-12 wenzelm 2008-04-12 replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression); pred_def: tag internal;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-20 wenzelm 2008-03-20 renamed former get_thms(_silent) to get_fact(_silent);
2008-03-17 wenzelm 2008-03-17 closeup: recover original order of free variables!
2008-03-05 wenzelm 2008-03-05 closeup: minor tuning of term traversal;
2007-12-17 haftmann 2007-12-17 explicit closing of derived witnesses
2007-12-13 haftmann 2007-12-13 memorizing and exporting destruction rules
2007-11-08 wenzelm 2007-11-08 avoid "import" as identifier, which is a keyword in Alice;
2007-11-05 ballarin 2007-11-05 Use of export rather than standard in interpretation.
2007-11-02 haftmann 2007-11-02 generic tactic Method.intros_tac
2007-10-19 ballarin 2007-10-19 Interpretation equations may have name and/or attribute; improved printing of types in interpretations.
2007-10-17 wenzelm 2007-10-17 locale pred: authentic syntax, tuned aprop_tr' accordingly;
2007-10-17 wenzelm 2007-10-17 clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');
2007-10-15 haftmann 2007-10-15 canonical interpretation interface
2007-10-12 haftmann 2007-10-12 tuned
2007-10-10 wenzelm 2007-10-10 removed redundant strip_vars/abs_eqn, use improved Drule.abs_def instead; renamed cert_instantiations to check_instantiations, check input only once (simultaneously!);
2007-10-10 ballarin 2007-10-10 Prepare proper interface of interpretation_i, interpret_i.
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-01 ballarin 2007-10-01 Theory/context data restructured; simplified interface for printing of interpretations.
2007-09-29 haftmann 2007-09-29 exported intern_expr