src/Provers/splitter.ML
Thu, 17 Apr 2008 22:22:21 +0200 wenzelm prove_global: pass context;
Tue, 25 Sep 2007 13:28:37 +0200 wenzelm Syntax.parse/check/read;
Sun, 06 May 2007 21:49:23 +0200 haftmann tuned
Sat, 14 Apr 2007 17:35:52 +0200 wenzelm cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
Wed, 04 Apr 2007 23:29:33 +0200 wenzelm rep_thm/cterm/ctyp: removed obsolete sign field;
Wed, 04 Apr 2007 00:11:03 +0200 wenzelm removed obsolete sign_of/sign_of_thm;
Mon, 18 Dec 2006 08:21:35 +0100 haftmann switched argument order in *.syntax lifters
Wed, 29 Nov 2006 15:44:51 +0100 wenzelm simplified method setup;
Thu, 21 Sep 2006 19:04:20 +0200 wenzelm member (op =);
Thu, 27 Jul 2006 14:21:57 +0200 webertj type annotation added to make SML/NJ happy
Wed, 26 Jul 2006 19:23:04 +0200 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
Fri, 10 Feb 2006 02:22:16 +0100 wenzelm Args/Attrib syntax: Context.generic;
Sat, 21 Jan 2006 23:02:14 +0100 wenzelm simplified type attribute;
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Sat, 14 Jan 2006 22:25:34 +0100 wenzelm generic attributes;
Tue, 03 Jan 2006 00:06:26 +0100 wenzelm avoid hardwired Trueprop;
Thu, 10 Nov 2005 20:57:11 +0100 wenzelm renamed Thm.cgoal_of to Thm.cprem_of;
Fri, 28 Oct 2005 22:27:47 +0200 wenzelm accomodate simplified Thm.lift_rule;
Fri, 21 Oct 2005 18:14:38 +0200 wenzelm OldGoals;
Mon, 17 Oct 2005 23:10:19 +0200 wenzelm functor: no Simplifier argument;
Mon, 12 Sep 2005 18:20:32 +0200 haftmann introduced new-style AList operations
Mon, 29 Aug 2005 16:18:04 +0200 wenzelm use AList operations;
Thu, 28 Jul 2005 15:19:51 +0200 wenzelm Sign.typ_match;
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.
Tue, 01 Jun 2004 12:33:50 +0200 wenzelm removed obsolete sort 'logic';
Thu, 13 Mar 2003 18:54:38 +0100 berghofe split_name no longer uses Sign.string_of_typ to encode types, since
Tue, 11 Mar 2003 14:13:20 +0100 berghofe addsplits / delsplits no longer ignore type of constant.
Fri, 17 May 2002 11:25:07 +0200 nipkow allowed more general split rules to cope with div/mod 2
Sun, 07 Jan 2001 21:41:56 +0100 wenzelm CHANGED_PROP;
Wed, 13 Dec 2000 09:30:59 +0100 nipkow sar split method uses new gen_split_tac.
Tue, 07 Nov 2000 17:41:29 +0100 berghofe Added type constraint in theorem "lift".
Mon, 06 Nov 2000 22:50:01 +0100 wenzelm Sign.typ_instance;
Tue, 19 Sep 2000 23:53:00 +0200 wenzelm tuned args;
Wed, 13 Sep 2000 22:31:19 +0200 wenzelm Args.addN, Args.delN;
Thu, 07 Sep 2000 20:56:58 +0200 wenzelm tuned msgs;
Sat, 02 Sep 2000 21:51:58 +0200 wenzelm "split": added "(asm)" option;
Mon, 28 Aug 2000 20:29:56 +0200 wenzelm added 'split' method;
Thu, 06 Jul 2000 15:36:59 +0200 nipkow Now two split thms for same constant at different types is allowed.
Fri, 05 May 2000 22:32:25 +0200 wenzelm use Args.colon / Args.parens;
Fri, 31 Mar 2000 21:55:27 +0200 wenzelm use Attrib.add_del_args;
Wed, 15 Mar 2000 18:52:07 +0100 wenzelm made SML/XL happy;
Wed, 15 Mar 2000 18:38:52 +0100 wenzelm added attributes, method modifiers, theory setup;
Fri, 01 Oct 1999 10:23:13 +0200 berghofe - Fixed bug in mk_split_pack which caused application of expansion theorem
Thu, 14 Jan 1999 13:20:02 +0100 nipkow Fixed old bug: selection of constant to be split should depend not just on
Thu, 24 Sep 1998 17:17:14 +0200 oheimb renamed mk_meta_eq to mk_eq
Tue, 08 Sep 1998 17:07:39 +0200 oheimb added caveat; a real solution would be difficult
Wed, 12 Aug 1998 16:21:18 +0200 oheimb the splitter is now defined as a functor
Thu, 14 May 1998 16:50:09 +0200 oheimb extended addsplits and delsplits to handle also split rules for assumptions
Sat, 28 Feb 1998 15:40:50 +0100 nipkow Little reorganization. Loop tactics have names now.
Wed, 07 Jan 1998 13:55:29 +0100 wenzelm adapted to new sort function;
Fri, 19 Dec 1997 10:33:59 +0100 wenzelm pasted old insertion sort (does not work with new sort function!)
Tue, 18 Nov 1997 15:30:50 +0100 berghofe Fixed bug in inst_split.
Mon, 17 Nov 1997 09:52:20 +0100 berghofe Tuned function mk_cntxt_splitthm.
Wed, 12 Nov 1997 12:22:56 +0100 oheimb renamed split_prem_tac to split_asm_tac
Fri, 07 Nov 1997 18:05:25 +0100 oheimb added split_prem_tac
Fri, 17 Oct 1997 15:23:14 +0200 nipkow Added error messages.
Fri, 10 Oct 1997 15:52:12 +0200 wenzelm fixed dots;
Tue, 22 Jul 1997 11:12:55 +0200 paulson Removal of the tactical STATE
Thu, 28 Nov 1996 10:44:24 +0100 paulson Replaced map...~~ by ListPair.map
less more (0) -60 tip