src/Provers/blast.ML
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-06 wenzelm 2010-03-06 eliminated Args.bang_facts (legacy feature);
2009-11-01 wenzelm 2009-11-01 modernized structure Context_Rules;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-24 wenzelm 2009-07-24 renamed functor BlastFun to Blast, require explicit theory; eliminated src/FOL/blastdata.ML;
2009-07-24 wenzelm 2009-07-24 explicit OldGoals;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-06 wenzelm 2009-07-06 structure Thm: less pervasive names;
2009-03-26 wenzelm 2009-03-26 simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-20 wenzelm 2009-03-20 Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-17 wenzelm 2009-03-17 renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
2009-03-15 wenzelm 2009-03-15 simplified method setup;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-03-06 wenzelm 2009-03-06 eliminated Output.immediate_output -- violates the official message channel protocol;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-03-01 wenzelm 2009-03-01 end_timing: generalized result -- message plus with explicit time values;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 tuned comments;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2007-11-09 wenzelm 2007-11-09 avoid obsolete Sign.read_prop;
2007-08-01 wenzelm 2007-08-01 simplified internal Config interface;
2007-07-31 wenzelm 2007-07-31 replaced depth_limit ref by blast_depth_limit configuration option; tuned method setup;
2007-07-29 wenzelm 2007-07-29 explicit global state argument -- no longer CRITICAL;
2007-07-25 wenzelm 2007-07-25 NAMED_CRITICAL;
2007-07-24 wenzelm 2007-07-24 marked some CRITICAL sections;
2007-07-22 wenzelm 2007-07-22 blast_hyp_subst_tac: plain bool argument;
2007-07-05 wenzelm 2007-07-05 simplified ObjectLogic.atomize;
2007-04-14 wenzelm 2007-04-14 Term.string_of_vname;
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2007-04-04 wenzelm 2007-04-04 cleaned-up Output functions;
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;