src/Provers/blast.ML
Tue, 14 Feb 2006 13:03:00 +0100 paulson fixed tracing
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Sat, 31 Dec 2005 21:49:41 +0100 wenzelm explicitly reject consts *Goal*, *False*;
Fri, 30 Dec 2005 16:56:59 +0100 wenzelm avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
Wed, 16 Nov 2005 17:45:23 +0100 wenzelm Trueprop: use ObjectLogic.judgment etc.;
Mon, 14 Nov 2005 18:25:34 +0100 paulson removal of is_hol
Thu, 10 Nov 2005 20:57:16 +0100 wenzelm uncurried Consts.typargs;
Wed, 02 Nov 2005 14:46:53 +0100 wenzelm fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
Thu, 27 Oct 2005 13:54:40 +0200 wenzelm replaced Defs.monomorphic by Sign.monomorphic;
Sat, 08 Oct 2005 20:15:34 +0200 wenzelm minor tweaks for Poplog/PML;
Tue, 06 Sep 2005 08:30:43 +0200 haftmann introduced some new-style AList operations
Mon, 05 Sep 2005 08:14:35 +0200 haftmann introduced binding priority 1 for linear combinators etc.
Mon, 01 Aug 2005 19:20:30 +0200 wenzelm Defs.monomorphic;
Fri, 15 Jul 2005 15:35:28 +0200 obua optimize no_types_needed, remove exception handler
Tue, 12 Jul 2005 12:49:46 +0200 paulson experimental code to reduce the amount of type information in blast
Wed, 20 Apr 2005 22:43:52 +0200 gagern Added op in front of constructor for better parsing.
Thu, 07 Apr 2005 09:25:33 +0200 wenzelm reverted renaming of Some/None in comments and strings;
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.
Sun, 29 Aug 2004 17:36:39 +0200 webertj depth limit (previously hard-coded with a value of 20) made a reference
Mon, 21 Jun 2004 16:39:39 +0200 wenzelm immediate_output;
Wed, 09 Jun 2004 18:57:18 +0200 wenzelm prs: Output.output;
Mon, 15 Mar 2004 10:45:31 +0100 paulson more up-to-date error msg
Fri, 30 Aug 2002 16:42:45 +0200 paulson removal of blast.overloaded
Wed, 20 Feb 2002 00:53:53 +0100 wenzelm Symbol.bump_string;
Thu, 06 Dec 2001 00:42:24 +0100 wenzelm tuned xtra_netpair;
Wed, 05 Dec 2001 03:06:05 +0100 wenzelm tuned;
Mon, 03 Dec 2001 21:01:37 +0100 wenzelm removed questionable init_gensym;
Mon, 15 Oct 2001 20:36:04 +0200 wenzelm Tactic.orderlist;
Sun, 14 Oct 2001 20:04:05 +0200 wenzelm ObjectLogic.atomize_tac;
Fri, 16 Feb 2001 13:29:07 +0100 paulson Blast bug fix: now always duplicates when applying a haz rule,
Wed, 14 Feb 2001 13:26:46 +0100 paulson new function get_overloads
Mon, 06 Nov 2000 22:47:41 +0100 wenzelm tuned atomize_goal;
Fri, 01 Sep 2000 00:36:08 +0200 wenzelm Method.bang_sectioned_args';
Tue, 01 Aug 2000 11:57:09 +0200 wenzelm handle actual object-logic rules by atomizing the goal;
Wed, 28 Jun 2000 10:54:47 +0200 paulson warns of weak elim rules and ignores them
Sat, 25 Sep 1999 13:23:58 +0200 wenzelm simplified sectioned_args;
Tue, 21 Sep 1999 17:26:50 +0200 wenzelm setup for refined facts handling;
Wed, 18 Aug 1999 20:47:31 +0200 wenzelm Method.modifier;
Mon, 02 Aug 1999 17:59:25 +0200 wenzelm blast method: optional depth argument;
Wed, 14 Jul 1999 13:05:46 +0200 wenzelm improved comment;
Fri, 09 Jul 1999 18:54:55 +0200 wenzelm type claset: added extra I/E rules;
Wed, 17 Mar 1999 16:33:47 +0100 wenzelm Theory.sign_of;
Wed, 25 Nov 1998 14:03:20 +0100 wenzelm replaced prs by std_output / writeln;
Wed, 18 Nov 1998 11:01:48 +0100 wenzelm method setup;
Fri, 23 Oct 1998 11:03:35 +0200 paulson occurs check now handles Bound variables (for soundness)
Mon, 05 Oct 1998 10:30:57 +0200 paulson MLWorks demands the "op" before $
Fri, 11 Sep 1998 16:31:40 +0200 paulson Less deterministic reconstruction: now more robust but perhaps slower
Thu, 10 Sep 1998 17:33:09 +0200 paulson Allows more backtracking in proof reconstruction, making it slower but more
Tue, 01 Sep 1998 10:10:27 +0200 paulson fixed error msg
Wed, 19 Aug 1998 10:49:30 +0200 paulson new version, more resistant to PROOF FAILED. Now it distinguishes between
Wed, 25 Feb 1998 20:29:58 +0100 oheimb renamed rep_claset to rep_cs
Wed, 25 Feb 1998 15:51:24 +0100 oheimb changed wrapper mechanism of classical reasoner
Fri, 02 Jan 1998 17:16:39 +0100 paulson Blast_tac now squashes flex-flex pairs immediately
Tue, 23 Dec 1997 11:39:03 +0100 paulson Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
Fri, 12 Dec 1997 10:34:21 +0100 paulson More deterministic and therefore faster (sometimes) proof reconstruction
Wed, 03 Dec 1997 11:42:45 +0100 paulson Fixed the treatment of substitution for equations, restricting occurrences of
Fri, 28 Nov 1997 10:52:04 +0100 paulson Printing of statistics including time for search & reconstruction
Wed, 26 Nov 1997 16:49:54 +0100 paulson Statistics
less more (0) -60 tip