src/Pure/Isar/local_defs.ML
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;