src/Provers/blast.ML
2006-11-10 wenzelm 2006-11-10 tuned names of start_timing,/end_timing/check_timer;
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-04-29 wenzelm 2006-04-29 tuned;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-02-14 paulson 2006-02-14 fixed tracing
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-12-31 wenzelm 2005-12-31 explicitly reject consts *Goal*, *False*;
2005-12-30 wenzelm 2005-12-30 avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
2005-11-16 wenzelm 2005-11-16 Trueprop: use ObjectLogic.judgment etc.; uniform Const of name * typargs, removed TConst;
2005-11-14 paulson 2005-11-14 removal of is_hol
2005-11-10 wenzelm 2005-11-10 uncurried Consts.typargs;
2005-11-02 wenzelm 2005-11-02 fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
2005-10-27 wenzelm 2005-10-27 replaced Defs.monomorphic by Sign.monomorphic;
2005-10-08 wenzelm 2005-10-08 minor tweaks for Poplog/PML;
2005-09-06 haftmann 2005-09-06 introduced some new-style AList operations
2005-09-05 haftmann 2005-09-05 introduced binding priority 1 for linear combinators etc.
2005-08-01 wenzelm 2005-08-01 Defs.monomorphic;
2005-07-15 obua 2005-07-15 optimize no_types_needed, remove exception handler
2005-07-12 paulson 2005-07-12 experimental code to reduce the amount of type information in blast
2005-04-20 gagern 2005-04-20 Added op in front of constructor for better parsing.
2005-04-07 wenzelm 2005-04-07 reverted renaming of Some/None in comments and strings;
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-08-29 webertj 2004-08-29 depth limit (previously hard-coded with a value of 20) made a reference
2004-06-21 wenzelm 2004-06-21 immediate_output;
2004-06-09 wenzelm 2004-06-09 prs: Output.output;
2004-03-15 paulson 2004-03-15 more up-to-date error msg
2002-08-30 paulson 2002-08-30 removal of blast.overloaded
2002-02-20 wenzelm 2002-02-20 Symbol.bump_string;
2001-12-06 wenzelm 2001-12-06 tuned xtra_netpair;
2001-12-05 wenzelm 2001-12-05 tuned;
2001-12-03 wenzelm 2001-12-03 removed questionable init_gensym;
2001-10-15 wenzelm 2001-10-15 Tactic.orderlist;
2001-10-14 wenzelm 2001-10-14 ObjectLogic.atomize_tac;
2001-02-16 paulson 2001-02-16 Blast bug fix: now always duplicates when applying a haz rule, whether or not new variables are added. Can now prove theorems such as these: val prems = Goal "[|P==>Q; P==>~Q|] ==> ~P"; by (blast_tac (claset() addDs prems) 1); val prems = Goal "[|Q==>P; ~Q==>P|] ==> P"; by (blast_tac (claset() addIs prems) 1);
2001-02-14 paulson 2001-02-14 new function get_overloads
2000-11-06 wenzelm 2000-11-06 tuned atomize_goal;
2000-09-01 wenzelm 2000-09-01 Method.bang_sectioned_args';
2000-08-01 wenzelm 2000-08-01 handle actual object-logic rules by atomizing the goal;
2000-06-28 paulson 2000-06-28 warns of weak elim rules and ignores them
1999-09-25 wenzelm 1999-09-25 simplified sectioned_args;
1999-09-21 wenzelm 1999-09-21 setup for refined facts handling; Method.bang_sectioned_args / Args.bang_facts;
1999-08-18 wenzelm 1999-08-18 Method.modifier;
1999-08-02 wenzelm 1999-08-02 blast method: optional depth argument;
1999-07-14 wenzelm 1999-07-14 improved comment;
1999-07-09 wenzelm 1999-07-09 type claset: added extra I/E rules;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1998-11-25 wenzelm 1998-11-25 replaced prs by std_output / writeln;
1998-11-18 wenzelm 1998-11-18 method setup;
1998-10-23 paulson 1998-10-23 occurs check now handles Bound variables (for soundness)
1998-10-05 paulson 1998-10-05 MLWorks demands the "op" before $
1998-09-11 paulson 1998-09-11 Less deterministic reconstruction: now more robust but perhaps slower
1998-09-10 paulson 1998-09-10 Allows more backtracking in proof reconstruction, making it slower but more robust (avoiding PROOF FAILED) Record type of branches, better tracing, etc.
1998-09-01 paulson 1998-09-01 fixed error msg
1998-08-19 paulson 1998-08-19 new version, more resistant to PROOF FAILED. Now it distinguishes between inferences that update the branch (resolve_tac) and those that do not (match_tac)
1998-02-25 oheimb 1998-02-25 renamed rep_claset to rep_cs
1998-02-25 oheimb 1998-02-25 changed wrapper mechanism of classical reasoner
1998-01-02 paulson 1998-01-02 Blast_tac now squashes flex-flex pairs immediately