src/Pure/Isar/object_logic.ML
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-15 wenzelm 2010-02-15 discontinued unnamed infix syntax;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-24 wenzelm 2009-10-24 tuned message;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in targets and derived elements;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-10-16 wenzelm 2008-10-16 Drule.norm_hhf_eqs;
2008-04-07 wenzelm 2008-04-07 renamed iterated forall_conv to params_conv;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2007-11-28 wenzelm 2007-11-28 added base_sort; added typedecl, dependent on base_sort (cf. intermediate typedecl.ML and former sign.ML, HOL/Tools/typedef_package.ML); typedecl: recovered proper use of Syntax.type_name;
2007-10-13 wenzelm 2007-10-13 replaced obsolete Theory.add_finals_i by Theory.add_deps;
2007-10-04 wenzelm 2007-10-04 replaced literal 'a by Name.aT;
2007-10-04 wenzelm 2007-10-04 Conv.forall_conv: proper context;
2007-07-29 wenzelm 2007-07-29 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-07-05 wenzelm 2007-07-05 tuned interfaces: atomize, atomize_prems, atomize_prems_tac; removed atomize_cterm/goal;
2007-07-05 wenzelm 2007-07-05 avoid polymorphic equality; added dest_judgment;
2007-07-04 wenzelm 2007-07-04 replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
2007-07-03 wenzelm 2007-07-03 CONVERSION tactical; MetaSimplifier.rewrite_goal_tac;
2007-05-10 wenzelm 2007-05-10 moved conversions to structure Conv;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-26 wenzelm 2007-04-26 renamed some old names Theory.xxx to Sign.xxx;
2006-12-07 wenzelm 2006-12-07 reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 wenzelm 2006-12-07 reorganized structure Goal vs. Tactic;
2006-10-09 wenzelm 2006-10-09 attribute: Context.mapping; removed Drule.strip_shyps_warning;
2006-03-14 wenzelm 2006-03-14 added is_elim (from Provers/classical.ML);
2006-02-06 wenzelm 2006-02-06 tuned;
2006-01-29 wenzelm 2006-01-29 moved treatment of object-logic equalities to local_defs.ML;
2006-01-28 wenzelm 2006-01-28 removed unatomize; added versions of meta_rewrite, unfold, fold;
2006-01-27 wenzelm 2006-01-27 renamed reverse_atomize to unatomize; added rulify_term/tac;
2006-01-25 wenzelm 2006-01-25 tuned atomize_cterm; added reverse_atomize_term/tac;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-04 wenzelm 2006-01-04 tuned;
2005-11-25 wenzelm 2005-11-25 forall_conv ~1;
2005-11-08 wenzelm 2005-11-08 renamed assert_prop to ensure_prop;
2005-10-18 wenzelm 2005-10-18 renamed atomize_rule to atomize_cterm;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; tuned;
2005-05-17 wenzelm 2005-05-17 tuned;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-23 skalberg 2004-06-23 Moved conversion rules from MetaSimplifier to Drule. refl_implies removed from Drule, instead imp_cong' exported from there.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-05-14 paulson 2004-05-14 conversion of theorems to atomic form
2003-10-10 skalberg 2003-10-10 Made judgments automatically declared final.
2002-07-16 wenzelm 2002-07-16 assert_propT;
2002-07-10 wenzelm 2002-07-10 added assert_judgment;
2002-05-31 berghofe 2002-05-31 Changed interface of MetaSimplifier.rewrite_term.
2002-01-21 wenzelm 2002-01-21 full_atomize;
2002-01-17 wenzelm 2002-01-17 atomize_term replaces atomize_cterm;
2002-01-12 wenzelm 2002-01-12 added atomize_cterm;
2002-01-12 wenzelm 2002-01-12 renamed forall_elim_vars_safe to gen_all;
2001-12-12 wenzelm 2001-12-12 drop_judgment: be graceful about undeclared judgment;
2001-12-05 wenzelm 2001-12-05 tuned;
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-09 wenzelm 2001-11-09 theory data: finish method;
2001-10-22 wenzelm 2001-10-22 moved object_logic.ML to Isar/object_logic.ML;