src/Provers/blast.ML
2002-02-20 ago Symbol.bump_string;
2001-12-06 ago tuned xtra_netpair;
2001-12-05 ago tuned;
2001-12-03 ago removed questionable init_gensym;
2001-10-15 ago Tactic.orderlist;
2001-10-14 ago ObjectLogic.atomize_tac;
2001-02-16 ago Blast bug fix: now always duplicates when applying a haz rule,
2001-02-14 ago new function get_overloads
2000-11-06 ago tuned atomize_goal;
2000-09-01 ago Method.bang_sectioned_args';
2000-08-01 ago handle actual object-logic rules by atomizing the goal;
2000-06-28 ago warns of weak elim rules and ignores them
1999-09-25 ago simplified sectioned_args;
1999-09-21 ago setup for refined facts handling;
1999-08-18 ago Method.modifier;
1999-08-02 ago blast method: optional depth argument;
1999-07-14 ago improved comment;
1999-07-09 ago type claset: added extra I/E rules;
1999-03-17 ago Theory.sign_of;
1998-11-25 ago replaced prs by std_output / writeln;
1998-11-18 ago method setup;
1998-10-23 ago occurs check now handles Bound variables (for soundness)
1998-10-05 ago MLWorks demands the "op" before $
1998-09-11 ago Less deterministic reconstruction: now more robust but perhaps slower
1998-09-10 ago Allows more backtracking in proof reconstruction, making it slower but more
1998-09-01 ago fixed error msg
1998-08-19 ago new version, more resistant to PROOF FAILED. Now it distinguishes between
1998-02-25 ago renamed rep_claset to rep_cs
1998-02-25 ago changed wrapper mechanism of classical reasoner
1998-01-02 ago Blast_tac now squashes flex-flex pairs immediately
1997-12-23 ago Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
1997-12-12 ago More deterministic and therefore faster (sometimes) proof reconstruction
1997-12-03 ago Fixed the treatment of substitution for equations, restricting occurrences of
1997-11-28 ago Printing of statistics including time for search & reconstruction
1997-11-26 ago Statistics
1997-11-21 ago changed Pure/Sequence interface -- isatool fixseq;
1997-11-20 ago Renamed "overload" to "overloaded" for sml/nj compatibility
1997-11-17 ago Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
1997-11-11 ago Now applies "map negOfGoal" to lits when expanding haz rules.
1997-11-05 ago fixed exception OPTION;
1997-11-03 ago adapted to new implicit claset mechanism;
1997-11-01 ago New treatment of overloading\!
1997-10-17 ago A lot of new comments
1997-07-18 ago tuned warning;
1997-06-19 ago Made proofs more concise by replacing calls to spy_analz_tac by uses of
1997-05-20 ago Basis library version of type "option" now resides in its own structure Option
1997-05-05 ago Again "norm" DOES NOT normalize bodies of abstractions
1997-05-02 ago More tracing. hyp_subst_tac allowed to fail
1997-04-30 ago More tracing; less exception handling
1997-04-24 ago refer to SOME, NONE on top-level;
1997-04-24 ago Addition of printed tracing. Also some tidying
1997-04-23 ago Loop detection: before expanding a haz formula, see whether it is a duplicate
1997-04-21 ago Penalty for branching instantiations reduced from log3 to log4.
1997-04-15 ago Changed penalty from log2 to log3
1997-04-09 ago Control over excessive branching by applying a log2 penalty
1997-04-04 ago Re-organization of the order of haz rules
1997-04-03 ago Now exports declConsts!
1997-04-02 ago Implementation of blast_tac: fast tableau prover