src/Pure/Isar/rule_cases.ML
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.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-02-21 nipkow 2004-02-21 Transitive_Closure: added consumes and case_names attributes Isar: fixed parameter name handling in simulatneous induction which I had not done properly 2 years ago.
2002-10-21 berghofe 2002-10-21 Removed Logic.skip_flexpairs.
2002-10-07 nipkow 2002-10-07 take/drop -> splitAt
2002-09-30 nipkow 2002-09-30 modified induct method
2002-07-26 wenzelm 2002-07-26 support for split assumptions in cases (hyps vs. prems);
2002-01-17 wenzelm 2002-01-17 RuleCases.make interface based on term instead of thm;
2002-01-15 wenzelm 2002-01-15 save: be slightly more about absent tags; get/add: missing case_names default to numbers 1, 2, 3, ...;
2001-11-12 wenzelm 2001-11-12 added empty;
2001-10-31 wenzelm 2001-10-31 put_consumes: really overwrite existing tag;
2001-10-30 wenzelm 2001-10-30 removed obsolete make_raw;
2001-10-14 wenzelm 2001-10-14 use ObjectLogic;
2001-01-30 oheimb 2001-01-30 added foldln
2001-01-12 wenzelm 2001-01-12 made SML/NJ happy;
2001-01-11 wenzelm 2001-01-11 make_raw: do not AutoBind.drop_judgment;
2001-01-09 wenzelm 2001-01-09 avoid renaming of params in cases;
2001-01-07 wenzelm 2001-01-07 do not AutoBind.drop_judgment;
2001-01-06 wenzelm 2001-01-06 support ?case binding; tuned;
2000-11-28 wenzelm 2000-11-28 added consumes, consumes_default; added save; tuned;
2000-11-06 wenzelm 2000-11-06 make: open_parms argument;
2000-07-13 wenzelm 2000-07-13 make: opaq flag;
2000-05-05 wenzelm 2000-05-05 GPLed;