src/Pure/Isar/local_defs.ML
2011-11-08 ago more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
2011-11-08 ago clarified Local_Defs.export: avoid costly still_fixed test, return all defs;
2011-04-28 ago eliminated slightly odd Proof_Context.bind_fixes;
2011-04-27 ago more precise positions via binding;
2011-04-27 ago tuned signature -- eliminated odd comment;
2011-04-27 ago more uniform Variable.add_frees/add_fixed etc.;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago tuned signature, disentangled dependencies;
2010-12-17 ago renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-10-28 ago tuned messages;
2010-09-05 ago pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
2010-03-13 ago Local_Defs.contract convenience;
2010-03-11 ago more basic Local_Defs.export_cterm;
2010-03-07 ago modernized structure Local_Defs;
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-11-02 ago modernized structure Primitive_Defs;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-06-24 ago renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-03-28 ago renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-19 ago use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-12 ago Assumption.all_prems_of, Assumption.all_assms_of;
2009-03-11 ago Thm.def_binding_optional;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago 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;
2009-03-03 ago Thm.binding;
2009-01-21 ago binding is alias for Binding.T
2009-01-11 ago stripped Id
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-03-27 ago eliminated theory ProtoPure;
2007-10-20 ago added fixed_abbrev;
2007-10-19 ago tuned interfaces;
2007-10-14 ago added add_def;
2007-10-11 ago added export_cterm;
2007-10-11 ago dest/cert_def: replaced Pretty.pp by explicit Proof.context;
2007-10-11 ago moved ProofContext.pp to Syntax.pp;
2007-08-14 ago PrimitiveDefs.dest/abs_def;
2007-07-29 ago renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-07-03 ago exported meta_rewrite_conv;
2007-05-10 ago moved conversions to structure Conv;
2007-05-07 ago simplified DataFun interfaces;
2007-04-15 ago Thm.fold_terms;
2007-04-14 ago tuned signature;
2007-04-03 ago renamed Variable.import to import_thms (avoid clash with Alice keywords);
2006-12-14 ago added trans_terms/props;
2006-12-12 ago tuned expand_term;
2006-12-07 ago reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 ago expand_term: based on Envir.expand_term;
2006-12-07 ago reorganized structure Goal vs. Tactic;
2006-12-06 ago added expand;
2006-11-29 ago added export;
2006-11-28 ago simplified '?' operator;
2006-11-23 ago prefer Proof.context over Context.generic;
2006-10-11 ago add_defs: declare terms;
2006-10-09 ago simplified derived_def;
2006-10-07 ago replaced add_def by more elaborate add_defs;
2006-08-02 ago normalized Proof.context/method type aliases;
2006-07-27 ago moved basic assumption operations from structure ProofContext to Assumption;