src/Pure/Isar/local_defs.ML
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-10-28 wenzelm 2010-10-28 tuned messages;
2010-09-05 wenzelm 2010-09-05 pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
2010-03-13 wenzelm 2010-03-13 Local_Defs.contract convenience;
2010-03-11 wenzelm 2010-03-11 more basic Local_Defs.export_cterm;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-02 wenzelm 2009-11-02 modernized structure Primitive_Defs;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-06-24 wenzelm 2009-06-24 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again);
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.add_fixes_i to ProofContext.add_fixes, 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 Assumption.all_prems_of, Assumption.all_assms_of;
2009-03-11 wenzelm 2009-03-11 Thm.def_binding_optional;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
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-03-03 wenzelm 2009-03-03 Thm.binding;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2009-01-11 haftmann 2009-01-11 stripped Id
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-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure;
2007-10-20 wenzelm 2007-10-20 added fixed_abbrev;
2007-10-19 wenzelm 2007-10-19 tuned interfaces;
2007-10-14 wenzelm 2007-10-14 added add_def;
2007-10-11 wenzelm 2007-10-11 added export_cterm; tuned;
2007-10-11 wenzelm 2007-10-11 dest/cert_def: replaced Pretty.pp by explicit Proof.context;
2007-10-11 wenzelm 2007-10-11 moved ProofContext.pp to Syntax.pp;
2007-08-14 wenzelm 2007-08-14 PrimitiveDefs.dest/abs_def;
2007-07-29 wenzelm 2007-07-29 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-07-03 wenzelm 2007-07-03 exported meta_rewrite_conv; CONVERSION tactical;
2007-05-10 wenzelm 2007-05-10 moved conversions to structure Conv;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-15 wenzelm 2007-04-15 Thm.fold_terms;
2007-04-14 wenzelm 2007-04-14 tuned signature; export: precomputed closure, no reference to contexts;
2007-04-03 wenzelm 2007-04-03 renamed Variable.import to import_thms (avoid clash with Alice keywords);
2006-12-14 wenzelm 2006-12-14 added trans_terms/props;
2006-12-12 wenzelm 2006-12-12 tuned expand_term;
2006-12-07 wenzelm 2006-12-07 reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 wenzelm 2006-12-07 expand_term: based on Envir.expand_term; tuned;
2006-12-07 wenzelm 2006-12-07 reorganized structure Goal vs. Tactic;
2006-12-06 wenzelm 2006-12-06 added expand; export: added explicit term operation;
2006-11-29 wenzelm 2006-11-29 added export; removed find_def, expand_defs;
2006-11-28 wenzelm 2006-11-28 simplified '?' operator; added expand_defs;
2006-11-23 wenzelm 2006-11-23 prefer Proof.context over Context.generic;
2006-10-11 wenzelm 2006-10-11 add_defs: declare terms;
2006-10-09 wenzelm 2006-10-09 simplified derived_def;
2006-10-07 wenzelm 2006-10-07 replaced add_def by more elaborate add_defs; added find_def (based on educated guesses);
2006-08-02 wenzelm 2006-08-02 normalized Proof.context/method type aliases; simplified Assumption/ProofContext.export;
2006-07-27 wenzelm 2006-07-27 moved basic assumption operations from structure ProofContext to Assumption;
2006-07-08 wenzelm 2006-07-08 Goal.prove: context;
2006-07-06 wenzelm 2006-07-06 def_export: Drule.generalize;
2006-06-15 wenzelm 2006-06-15 ProofContext: moved variable operations to struct Variable;
2006-05-07 wenzelm 2006-05-07 removed 'concl is' patterns;
2006-02-06 wenzelm 2006-02-06 cert_def: use Logic.dest_def; moved abs_def to logic.ML; derived_def: conditional flag;
2006-02-02 wenzelm 2006-02-02 tuned comments;
2006-01-31 wenzelm 2006-01-31 (un)fold: no raw flag; tuned;
2006-01-31 wenzelm 2006-01-31 export meta_rewrite_rule; tuned;