src/Provers/blast.ML
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
Fri, 21 Nov 1997 15:29:56 +0100 wenzelm changed Pure/Sequence interface -- isatool fixseq;
Thu, 20 Nov 1997 10:54:04 +0100 paulson Renamed "overload" to "overloaded" for sml/nj compatibility
Mon, 17 Nov 1997 10:48:07 +0100 paulson Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
Tue, 11 Nov 1997 11:12:37 +0100 paulson Now applies "map negOfGoal" to lits when expanding haz rules.
Wed, 05 Nov 1997 11:45:51 +0100 wenzelm fixed exception OPTION;
Mon, 03 Nov 1997 11:56:17 +0100 wenzelm adapted to new implicit claset mechanism;
Sat, 01 Nov 1997 13:02:39 +0100 paulson New treatment of overloading\!
Fri, 17 Oct 1997 11:12:36 +0200 paulson A lot of new comments
Fri, 18 Jul 1997 13:54:41 +0200 wenzelm tuned warning;
Thu, 19 Jun 1997 11:31:14 +0200 paulson Made proofs more concise by replacing calls to spy_analz_tac by uses of
Tue, 20 May 1997 11:47:33 +0200 paulson Basis library version of type "option" now resides in its own structure Option
Mon, 05 May 1997 12:15:20 +0200 paulson Again "norm" DOES NOT normalize bodies of abstractions
Fri, 02 May 1997 10:18:50 +0200 paulson More tracing. hyp_subst_tac allowed to fail
Wed, 30 Apr 1997 12:59:24 +0200 paulson More tracing; less exception handling
Thu, 24 Apr 1997 19:47:53 +0200 wenzelm refer to SOME, NONE on top-level;
Thu, 24 Apr 1997 11:21:46 +0200 paulson Addition of printed tracing. Also some tidying
Wed, 23 Apr 1997 11:11:38 +0200 paulson Loop detection: before expanding a haz formula, see whether it is a duplicate
Mon, 21 Apr 1997 10:16:01 +0200 paulson Penalty for branching instantiations reduced from log3 to log4.
Tue, 15 Apr 1997 10:22:50 +0200 paulson Changed penalty from log2 to log3
Wed, 09 Apr 1997 12:36:52 +0200 paulson Control over excessive branching by applying a log2 penalty
Fri, 04 Apr 1997 11:28:28 +0200 paulson Re-organization of the order of haz rules
Thu, 03 Apr 1997 10:32:34 +0200 paulson Now exports declConsts!
Wed, 02 Apr 1997 11:15:46 +0200 paulson Implementation of blast_tac: fast tableau prover
less more (0) tip