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