src/Tools/induct.ML
Tue, 19 Aug 2014 12:05:11 +0200 wenzelm simplified type Proof.method;
Mon, 31 Mar 2014 12:35:39 +0200 wenzelm some shortcuts for chunks, which sometimes avoid bulky string output;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Thu, 20 Mar 2014 21:07:57 +0100 wenzelm enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
Thu, 06 Mar 2014 13:44:01 +0100 wenzelm more uniform check_const/read_const;
Thu, 06 Mar 2014 12:10:19 +0100 wenzelm tuned signature -- more uniform check_type_name/read_type_name;
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Fri, 23 Aug 2013 17:01:12 +0200 wenzelm tuned signature;
Sat, 27 Jul 2013 16:35:51 +0200 wenzelm standardized aliases;
Wed, 17 Jul 2013 13:45:55 +0200 wenzelm take context from static theory, not dynamic theory certificate;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Tue, 09 Apr 2013 15:29:25 +0200 wenzelm discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
Sat, 30 Mar 2013 13:40:19 +0100 wenzelm more item markup;
Fri, 29 Mar 2013 22:14:27 +0100 wenzelm Pretty.item markup for improved readability of lists of items;
Tue, 09 Oct 2012 20:05:17 +0200 wenzelm clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional;
Sat, 29 Sep 2012 18:23:46 +0200 wenzelm more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
Wed, 21 Mar 2012 11:00:34 +0100 wenzelm prefer explicitly qualified exception List.Empty;
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
Sun, 06 Nov 2011 21:51:46 +0100 wenzelm more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
Thu, 03 Nov 2011 22:51:37 +0100 wenzelm tuned signature;
Sun, 16 Oct 2011 18:48:30 +0200 wenzelm added Term.dummy_pattern conveniences;
Wed, 12 Oct 2011 22:21:38 +0200 wenzelm tuned signature;
Wed, 12 Oct 2011 21:39:33 +0200 wenzelm misc tuning and clarification;
Wed, 12 Oct 2011 20:57:40 +0200 wenzelm tuned ML style;
Tue, 20 Sep 2011 05:47:11 +0200 nipkow New proof method "induction" that gives induction hypotheses the name IH.
Fri, 16 Sep 2011 09:18:15 +0200 nipkow when applying induction rules, remove names of assumptions that come
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Thu, 09 Jun 2011 23:12:02 +0200 wenzelm renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
Thu, 09 Jun 2011 17:51:49 +0200 wenzelm simplified Name.variant -- discontinued builtin fold_map;
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript;
Wed, 27 Apr 2011 17:58:45 +0200 wenzelm reorganized fixes as specialized (global) name space;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Fri, 17 Dec 2010 17:08:56 +0100 wenzelm renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
Wed, 25 Aug 2010 18:36:22 +0200 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
Thu, 24 Jun 2010 12:24:35 +0200 wenzelm misc tuning;
Thu, 24 Jun 2010 12:16:39 +0200 wenzelm tuned auxiliary structures;
Thu, 24 Jun 2010 11:28:34 +0200 wenzelm Net.encode_type;
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Fri, 30 Apr 2010 23:43:09 +0200 wenzelm slightly more standard induct_simp_add/del attributes;
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Sun, 07 Mar 2010 11:57:16 +0100 wenzelm modernized structure Local_Defs;
Sat, 27 Feb 2010 20:55:18 +0100 wenzelm type/const name: explicitly allow abbreviations as well;
Thu, 25 Feb 2010 22:06:43 +0100 wenzelm clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
Sat, 30 Jan 2010 16:58:46 +0100 berghofe Added infrastructure for simplifying equality constraints in cases rules.
Sun, 10 Jan 2010 18:01:04 +0100 berghofe Added infrastructure for simplifying equality constraints.
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Sun, 01 Nov 2009 20:59:34 +0100 wenzelm adapted Item_Net;
Sun, 01 Nov 2009 15:24:45 +0100 wenzelm modernized structure Rule_Cases;
Thu, 29 Oct 2009 13:21:38 +0100 wenzelm separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
Fri, 02 Oct 2009 22:15:08 +0200 wenzelm eliminated dead code;
Fri, 28 Aug 2009 21:04:03 +0200 wenzelm modernized messages -- eliminated ctyp/cterm operations;
Sat, 25 Jul 2009 12:43:45 +0200 wenzelm eliminated redundant Library.multiply;
Fri, 24 Jul 2009 12:33:00 +0200 wenzelm renamed functor InductFun to Induct;
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Fri, 17 Jul 2009 21:33:00 +0200 wenzelm tuned/modernized Envir operations;
Thu, 26 Mar 2009 14:14:02 +0100 wenzelm simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
Tue, 17 Mar 2009 14:12:43 +0100 wenzelm adapted to general Item_Net;
less more (0) -60 tip