2010-04-26 ago eliminanated some unreferenced identifiers;
2010-03-07 ago modernized structure Object_Logic;
2010-02-27 ago modernized structure Term_Ord;
2010-01-30 ago Added "constraints" tag / attribute for specifying the number of equality
2010-01-15 ago Eliminated is_open option of Rule_Cases.make_nested/make_common;
2009-12-09 ago explicit lower bound for index
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop
2009-11-01 ago modernized structure Rule_Cases;
2009-10-29 ago separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
2009-06-24 ago renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2008-12-31 ago moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
2008-08-14 ago moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-05-16 ago removed unused make_simple;
2008-04-15 ago Library.is_equal;
2007-10-05 ago export get_consumes;
2007-08-13 ago Lexicon.read_indexname/nat/variable;
2007-07-08 ago thm tag: list;
2007-07-05 ago tuned goal conversion interfaces;
2007-07-03 ago replaced Conv.goals_conv by Conv.prems_conv;
2007-06-19 ago balanced conjunctions;
2007-05-10 ago moved conversions to structure Conv;
2007-04-03 ago renamed Variable.import to import_thms (avoid clash with Alice keywords);
2006-12-10 ago extract_case: Name.clean;
2006-12-07 ago reorganized structure Tactic vs. MetaSimplifier;
2006-12-05 ago thm/prf: separate official name vs. additional tags;
2006-11-29 ago simplified Logic.count_prems;
2006-11-16 ago moved some fundamental concepts to General/basics.ML;
2006-08-02 ago normalized Proof.context/method type aliases;
2006-07-26 ago Variable.import(T): result includes fixed types/terms;
2006-07-11 ago Name.internal;
2006-06-17 ago mutual_rule: proper context;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-13 ago use conjunction stuff from conjunction.ML;
2006-02-15 ago removed distinct, renamed gen_distinct to distinct;
2006-02-11 ago tuned;
2006-02-02 ago consumes: negative argument relative to total number of prems;
2006-01-27 ago moved theorem tags from Drule to PureThy;
2006-01-21 ago simplified type attribute;
2006-01-07 ago support nested cases;
2006-01-05 ago added strict_mutual_rule;
2005-12-22 ago consume: expand defs in prems of concls;
2005-12-08 ago removed Syntax.deskolem;
2005-11-25 ago consume: unfold defs in all major prems;
2005-11-23 ago consume: proper treatment of defs;
2005-11-22 ago added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
2005-11-16 ago added THEN_ALL_NEW_CASES;
2005-10-31 ago fold_index replacing foldln
2005-10-15 ago export strip_params;
2005-09-13 ago added simple;
2005-08-29 ago use AList operations;
2005-08-28 ago unskolem local vars;
2005-08-18 ago added NO_CASES;
2005-06-14 ago added type tactic;
2005-05-31 ago make: T option -- actually remove undefined cases;
2005-05-17 ago tuned;
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.