src/FOLP/simp.ML
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-27 wenzelm 2009-10-27 eliminated some old folds;
2009-10-22 haftmann 2009-10-22 map_range (and map_index) combinator
2009-10-21 haftmann 2009-10-21 removed old-style \ and \\ infixes
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-08-29 wenzelm 2009-08-29 eliminated hard tabs;
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-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read;
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2006-11-10 wenzelm 2006-11-10 tuned Variable.trade;
2006-10-20 haftmann 2006-10-20 slight cleanup
2006-10-10 haftmann 2006-10-10 gen_rem(s) abandoned in favour of remove / subtract
2006-07-25 wenzelm 2006-07-25 renamed Term.variant_abs to Syntax.variant_abs;
2006-06-19 wenzelm 2006-06-19 eliminated freeze/varify in favour of Variable.import/export/trade;
2006-06-13 wenzelm 2006-06-13 tuned;
2006-06-07 wenzelm 2006-06-07 do not open Logic;
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-07-28 wenzelm 2005-07-28 Sign.typ_instance;
2005-07-19 wenzelm 2005-07-19 Logic.incr_tvar;
2005-07-13 wenzelm 2005-07-13 improved Net interface;
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-05-21 wenzelm 2004-05-21 Type.typ_instance;
2004-04-22 wenzelm 2004-04-22 tuned;
2002-05-07 wenzelm 2002-05-07 use eq_thm_prop instead of slightly inadequate eq_thm;
1999-09-29 wenzelm 1999-09-29 Sign.defaultS;
1999-07-10 wenzelm 1999-07-10 handle THM exn;
1998-11-25 wenzelm 1998-11-25 replaced prs by std_output;
1997-11-21 wenzelm 1997-11-21 changed Pure/Sequence interface -- isatool fixseq;
1997-07-22 paulson 1997-07-22 Removal of the tactical STATE
1996-11-28 paulson 1996-11-28 Replaced map...~~ by ListPair.map
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-01-29 clasohm 1996-01-29 expanded tabs
1994-09-14 wenzelm 1994-09-14 now uses Sign.const_type;
1994-01-18 lcp 1994-01-18 Updated refs to old Sign functions
1993-09-16 clasohm 1993-09-16 Initial revision