src/Pure/Isar/object_logic.ML
2011-11-06 ago more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-16 ago modernized structure Proof_Context;
2011-01-15 ago clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
2011-01-10 ago added merge_options convenience;
2010-12-17 ago renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-07 ago separate structure Typedecl;
2010-03-07 ago modernized structure Object_Logic;
2010-02-15 ago discontinued unnamed infix syntax;
2009-11-08 ago adapted Theory_Data;
2009-10-24 ago tuned message;
2009-03-07 ago more uniform handling of binding in targets and derived elements;
2009-01-21 ago removed Ids;
2008-12-04 ago cleaned up binding module and related code
2008-10-16 ago Drule.norm_hhf_eqs;
2008-04-07 ago renamed iterated forall_conv to params_conv;
2008-03-28 ago Context.>> : operate on Context.generic;
2008-03-27 ago eliminated delayed theory setup
2007-11-28 ago added base_sort;
2007-10-13 ago replaced obsolete Theory.add_finals_i by Theory.add_deps;
2007-10-04 ago replaced literal 'a by Name.aT;
2007-10-04 ago Conv.forall_conv: proper context;
2007-07-29 ago renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-07-05 ago tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
2007-07-05 ago avoid polymorphic equality;
2007-07-04 ago replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
2007-07-03 ago CONVERSION tactical;
2007-05-10 ago moved conversions to structure Conv;
2007-05-07 ago simplified DataFun interfaces;
2007-04-26 ago renamed some old names Theory.xxx to Sign.xxx;
2006-12-07 ago reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 ago reorganized structure Goal vs. Tactic;
2006-10-09 ago attribute: Context.mapping;
2006-03-14 ago added is_elim (from Provers/classical.ML);
2006-02-06 ago tuned;
2006-01-29 ago moved treatment of object-logic equalities to local_defs.ML;
2006-01-28 ago removed unatomize;
2006-01-27 ago renamed reverse_atomize to unatomize;
2006-01-25 ago tuned atomize_cterm;
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2006-01-04 ago tuned;
2005-11-25 ago forall_conv ~1;
2005-11-08 ago renamed assert_prop to ensure_prop;
2005-10-18 ago renamed atomize_rule to atomize_cterm;
2005-06-17 ago accomodate change of TheoryDataFun;
2005-05-17 ago tuned;
2005-04-21 ago superceded by Pure.thy and CPure.thy;
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-06-23 ago Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-01 ago removed obsolete sort 'logic';
2004-05-14 ago conversion of theorems to atomic form
2003-10-10 ago Made judgments automatically declared final.
2002-07-16 ago assert_propT;
2002-07-10 ago added assert_judgment;
2002-05-31 ago Changed interface of MetaSimplifier.rewrite_term.