2007-08-20 ago TextIO.inputLine: non-critical (assume exclusive ownership);
2007-07-23 ago marked some CRITICAL sections (for multithreading);
2007-07-05 ago tuned goal conversion interfaces;
2007-07-03 ago CONVERSION: handle TYPE | TERM | CTERM | THM;
2007-07-03 ago added CONVERSION tactical;
2007-06-14 ago tidied
2007-06-03 ago added CSUBGOAL;
2007-05-31 ago simplified/unified list fold;
2007-05-31 ago TextIO.inputLine: use present SML B library version;
2007-04-04 ago rep_thm/cterm/ctyp: removed obsolete sign field;
2007-02-26 ago moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2006-09-21 ago member (op =);
2006-07-25 ago renamed Term.variant_abs to Syntax.variant_abs;
2006-06-12 ago tuned Seq/Envir/Unify interfaces;
2006-05-16 ago avoid low-level Term.str_of_term;
2006-04-24 ago cleaned up some diagnostic mathom
2006-03-10 ago METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
2006-02-28 ago splitting up METAHYPS into smaller functions
2005-10-21 ago moved SELECT_GOAL to goal.ML;
2005-09-13 ago Seq.maps;
2005-06-21 ago tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
2005-06-02 ago header;
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-07-06 ago print_tac now outputs goals through trace-channel
2004-06-25 ago Merging the meta-simplifier with the Provers-simplifier. Next step:
2002-10-21 ago No more explicit manipulation of flex-flex constraints in metahyps_aux_tac.
2002-10-17 ago fixing the cut_tac method to work when there are no instantiations and the
2002-05-07 ago tuned;
2002-01-26 ago generic DETERM;
2001-11-21 ago use tracing function for trace output;
2001-11-06 ago goals_limit moved to display.ML;
2001-10-23 ago added RANGE (from Isar/proof.ML);
2001-10-22 ago Display.print_goals;
2001-08-31 ago Tidied function SELECT_GOAL.
2001-01-07 ago CHANGED_PROP;
2001-01-03 ago Thm: dest_comb, dest_abs, capply, cabs no longer global;
2000-03-20 ago ALLGOALS_RANGE superceded by Seq.INTERVAL;
2000-03-08 ago export ALLGOALS_RANGE;
2000-03-04 ago added REPEAT_ALL_NEW;
2000-01-28 ago added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
1999-10-04 ago fixed CHANGED_GOAL, which is used by stac
1999-03-17 ago qualify Theory.sign_of etc.;
1998-12-28 ago Added a "message" argument to print_tac
1998-11-30 ago tactical CHANGED now uses alpha-eta conversion, not alpha conversion
1998-11-25 ago tuned space;
1998-11-25 ago replaced prs by writeln;
1998-11-17 ago Drule.rev_triv_goal;
1998-08-13 ago simpler SELECT_GOAL no longer inserts a dummy parameter
1998-07-14 ago CHANGED_GOAL added to declare a more robust stac
1998-02-05 ago added THEN_ALL_NEW;
1997-11-21 ago changed Sequence interface (now Seq, in seq.ML);
1997-10-24 ago ProtoPure.thy;
1997-09-11 ago removed print_goals_ref (which was broken anyway);
1997-07-23 ago Removal of tactical STATE
1997-03-18 ago A more explicit prefix because gensym now generates easily predicatable
1997-02-21 ago Replaced "flat" by the Basis Library function List.concat
1997-02-15 ago added THEN_MAYBE and THEN_MAYBE'
1997-02-04 ago Gradual switching to Basis Library functions nth, drop, etc.