src/Pure/Isar/locale.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
2007-09-24 wenzelm 2007-09-24 eliminated ProofContext.read_termTs;
2007-09-18 ballarin 2007-09-18 Morphisms applied in global interpretations behave correctly on types and terms.
2007-09-04 ballarin 2007-09-04 Improved comment.
2007-07-28 wenzelm 2007-07-28 tuned signature;
2007-07-27 wenzelm 2007-07-27 Druke.dummy_thm;
2007-07-23 ballarin 2007-07-23 interpretation: unfolding of equations; interpretation: equations are propositions not pairs of terms;
2007-07-08 wenzelm 2007-07-08 replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-05 wenzelm 2007-07-05 simplified ObjectLogic.atomize;
2007-06-19 wenzelm 2007-06-19 balanced conjunctions;
2007-06-03 wenzelm 2007-06-03 added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-26 wenzelm 2007-04-26 renamed some old names Theory.xxx to Sign.xxx;
2007-04-23 wenzelm 2007-04-23 read_instantiations: proper type-inference with fixed variables, infer parameter types as well; gen_prep_registration: removed unused read_terms (dead code!); tuned;
2007-04-20 ballarin 2007-04-20 Interpretation equations applied to attributes; code cleanup in read_instantiations
2007-04-15 wenzelm 2007-04-15 Thm.fold_terms; Syntax.mixfixT;
2007-04-14 wenzelm 2007-04-14 Term.string_of_vname;
2007-04-13 ballarin 2007-04-13 Experimental interpretation code for definitions.
2007-04-03 wenzelm 2007-04-03 avoid clash with Alice keywords;
2007-03-26 haftmann 2007-03-26 exported interface for intro rules
2007-02-23 haftmann 2007-02-23 locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
2007-02-19 schirmer 2007-02-19 more precise error message in parameter unification
2007-02-10 haftmann 2007-02-10 internal interfaces for interpretation and interpret
2007-02-04 wenzelm 2007-02-04 interpretation: attempt to be more serious about name_morphism;
2006-12-30 wenzelm 2006-12-30 removed conditional combinator;
2006-12-07 wenzelm 2006-12-07 reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 wenzelm 2006-12-07 tuned print_locale output; add_decls: Thm.internalK;
2006-12-06 wenzelm 2006-12-06 export: added explicit term operation;
2006-12-05 wenzelm 2006-12-05 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
2006-11-30 wenzelm 2006-11-30 Goal.norm/close_result;
2006-11-29 wenzelm 2006-11-29 *** bad commit -- reverted to previous version ***