src/Provers/induct_method.ML
Tue, 10 Jan 2006 19:33:30 +0100 wenzelm fix_tac: no warning;
Sat, 07 Jan 2006 12:26:25 +0100 wenzelm RuleCases.make_common/nested;
Thu, 05 Jan 2006 17:14:07 +0100 wenzelm RuleCases.strict_mutual_rule;
Fri, 23 Dec 2005 18:36:27 +0100 wenzelm removed obsolete atomize_old;
Fri, 23 Dec 2005 15:16:44 +0100 wenzelm proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;
Thu, 22 Dec 2005 00:28:51 +0100 wenzelm simplified setup: removed dest_concls, local_impI, conjI;
Fri, 02 Dec 2005 08:06:59 +0100 haftmann introduced new map2, fold
Tue, 29 Nov 2005 23:00:20 +0100 wenzelm moved nth_list to Pure/library.ML;
Fri, 25 Nov 2005 20:57:51 +0100 wenzelm induct: insert defs in object-logic form;
Fri, 25 Nov 2005 18:58:36 +0100 wenzelm fix_tac: proper treatment of major premises in goal;
Wed, 23 Nov 2005 22:23:52 +0100 wenzelm more robust revert_skolem;
Wed, 23 Nov 2005 18:52:02 +0100 wenzelm (co)induct: taking;
Tue, 22 Nov 2005 19:34:43 +0100 wenzelm make coinduct actually work;
Sat, 19 Nov 2005 14:21:02 +0100 wenzelm induct: CONJUNCTS for multiple goals;
Wed, 16 Nov 2005 17:45:24 +0100 wenzelm induct: support local definitions to be passed through the induction;
Thu, 10 Nov 2005 20:57:17 +0100 wenzelm induct method: fixes;
Fri, 28 Oct 2005 22:27:47 +0200 wenzelm accomodate simplified Thm.lift_rule;
Fri, 21 Oct 2005 18:14:41 +0200 wenzelm Goal.norm_hhf_rule, Goal.init;
Tue, 14 Jun 2005 21:56:57 +0200 wenzelm export cases_tac, induct_tac;
Thu, 21 Apr 2005 18:57:18 +0200 berghofe Adapted to new interface of instantiation and unification / matching functions.
Wed, 13 Apr 2005 18:46:04 +0200 wenzelm *** MESSAGE REFERS TO PREVIOUS VERSION ***
Wed, 13 Apr 2005 18:34:22 +0200 wenzelm *** empty log message ***
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 11 Oct 2004 07:39:19 +0200 nipkow Induction now preserves the name of the induction variable.
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Sat, 21 Feb 2004 08:43:08 +0100 nipkow Transitive_Closure: added consumes and case_names attributes
Mon, 30 Sep 2002 15:45:11 +0200 nipkow fixes !!-bound vars in induction statement automatically
Fri, 26 Jul 2002 21:09:39 +0200 wenzelm support for split assumptions in cases (hyps vs. prems);
Fri, 31 May 2002 18:49:31 +0200 berghofe Changed interface of MetaSimplifier.rewrite_term.
Tue, 07 May 2002 14:26:32 +0200 wenzelm use eq_thm_prop instead of slightly inadequate eq_thm;
Sat, 26 Jan 2002 19:17:15 +0100 wenzelm cases: really append cases_default;
Thu, 17 Jan 2002 21:02:18 +0100 wenzelm MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
Wed, 28 Nov 2001 00:38:11 +0100 wenzelm join_rules RuleCases.save;
Mon, 19 Nov 2001 20:46:05 +0100 wenzelm induct method: localize rews for rule;
Mon, 12 Nov 2001 23:30:16 +0100 wenzelm induct: rule_versions produces localized variants;
Mon, 12 Nov 2001 20:23:24 +0100 wenzelm proper handling of mutual rules (esp. for sets);
Mon, 05 Nov 2001 20:56:29 +0100 wenzelm Method.trace ctxt;
Wed, 31 Oct 2001 01:28:39 +0100 wenzelm induct: internalize ``missing'' consumes-facts from goal state
Tue, 30 Oct 2001 17:30:21 +0100 wenzelm induct: cases are extracted from rulified rule;
Tue, 16 Oct 2001 17:56:12 +0200 wenzelm dest_env: norm_term on rhs;
Tue, 16 Oct 2001 00:32:01 +0200 wenzelm simplified resolveq_cases_tac for cases, separate version for induct;
Mon, 15 Oct 2001 20:35:10 +0200 wenzelm Tactic.rewrite_cterm;
Sun, 14 Oct 2001 22:15:07 +0200 wenzelm moved rulify to ObjectLogic;
Sun, 14 Oct 2001 20:05:42 +0200 wenzelm use ObjectLogic stuff;
Fri, 12 Oct 2001 12:13:31 +0200 wenzelm removed vars_of, concls_of;
Thu, 04 Oct 2001 15:20:40 +0200 wenzelm proof by cases and induction on types and sets (used to be specific for HOL);
less more (0) tip