src/Pure/Isar/local_defs.ML
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;
2006-01-29 wenzelm 2006-01-29 added attributes defn_add/del; added (un)fold operations (from object_logic.ML); tuned;
2006-01-28 wenzelm 2006-01-28 Basic operations on local definitions.
2001-10-16 wenzelm 2001-10-16 simplified exporter interface;
2001-10-10 berghofe 2001-10-10 Removed unnecessary application of Drule.standard.
2000-11-13 wenzelm 2000-11-13 tuned statement args;
2000-07-30 wenzelm 2000-07-30 local_def(_i): no constraint on var; exporter setup;
2000-07-13 wenzelm 2000-07-13 use ProofContext.bind_skolem;
2000-07-13 wenzelm 2000-07-13 prep rhs in original context; tuned;
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-01-05 wenzelm 2000-01-05 prepare patterns only once;
1999-09-30 wenzelm 1999-09-30 local_def_i: typ option; admit additional (fixed) type vars on rhs;
1999-09-07 wenzelm 1999-09-07 tuned;
1999-09-01 wenzelm 1999-09-01 Thm.def_name;
1999-08-18 wenzelm 1999-08-18 assume: multiple args;
1999-07-13 wenzelm 1999-07-13 handle cgoal;
1999-07-09 wenzelm 1999-07-09 added Isar/local_defs.ML;