src/Pure/tctical.ML
2009-02-27 wenzelm 2009-02-27 tuned CHANGED_GOAL: use Thm.cprem_of instead of selecting from Thm.prems_of;
2008-12-31 wenzelm 2008-12-31 use regular Term.add_XXX etc.;
2008-12-31 wenzelm 2008-12-31 use regular Term.add_vars, Term.add_frees etc.;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-04-15 wenzelm 2008-04-15 Thm.forall_elim_var(s);
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2007-08-20 wenzelm 2007-08-20 TextIO.inputLine: non-critical (assume exclusive ownership);
2007-07-23 wenzelm 2007-07-23 marked some CRITICAL sections (for multithreading);
2007-07-05 wenzelm 2007-07-05 tuned goal conversion interfaces;
2007-07-03 wenzelm 2007-07-03 CONVERSION: handle TYPE | TERM | CTERM | THM;
2007-07-03 wenzelm 2007-07-03 added CONVERSION tactical; tuned signature;
2007-06-14 paulson 2007-06-14 tidied
2007-06-03 wenzelm 2007-06-03 added CSUBGOAL;
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-05-31 wenzelm 2007-05-31 TextIO.inputLine: use present SML B library version;
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-07-25 wenzelm 2006-07-25 renamed Term.variant_abs to Syntax.variant_abs;
2006-06-12 wenzelm 2006-06-12 tuned Seq/Envir/Unify interfaces;
2006-05-16 wenzelm 2006-05-16 avoid low-level Term.str_of_term;
2006-04-24 haftmann 2006-04-24 cleaned up some diagnostic mathom
2006-03-10 mengj 2006-03-10 METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
2006-02-28 paulson 2006-02-28 splitting up METAHYPS into smaller functions
2005-10-21 wenzelm 2005-10-21 moved SELECT_GOAL to goal.ML;
2005-09-13 wenzelm 2005-09-13 Seq.maps;
2005-06-21 wenzelm 2005-06-21 tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
2005-06-02 wenzelm 2005-06-02 header;
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-07-06 schirmer 2004-07-06 print_tac now outputs goals through trace-channel
2004-06-25 skalberg 2004-06-25 Merging the meta-simplifier with the Provers-simplifier. Next step: make the simplification procedure simpset-aware.
2002-10-21 berghofe 2002-10-21 No more explicit manipulation of flex-flex constraints in metahyps_aux_tac.
2002-10-17 paulson 2002-10-17 fixing the cut_tac method to work when there are no instantiations and the supplied theorems have premises
2002-05-07 wenzelm 2002-05-07 tuned;
2002-01-26 wenzelm 2002-01-26 generic DETERM;
2001-11-21 wenzelm 2001-11-21 use tracing function for trace output;
2001-11-06 wenzelm 2001-11-06 goals_limit moved to display.ML;
2001-10-23 wenzelm 2001-10-23 added RANGE (from Isar/proof.ML);
2001-10-22 wenzelm 2001-10-22 Display.print_goals;
2001-08-31 berghofe 2001-08-31 Tidied function SELECT_GOAL.
2001-01-07 wenzelm 2001-01-07 CHANGED_PROP;
2001-01-03 wenzelm 2001-01-03 Thm: dest_comb, dest_abs, capply, cabs no longer global;
2000-03-20 wenzelm 2000-03-20 ALLGOALS_RANGE superceded by Seq.INTERVAL;
2000-03-08 wenzelm 2000-03-08 export ALLGOALS_RANGE;
2000-03-04 wenzelm 2000-03-04 added REPEAT_ALL_NEW;
2000-01-28 oheimb 2000-01-28 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
1999-10-04 paulson 1999-10-04 fixed CHANGED_GOAL, which is used by stac
1999-03-17 wenzelm 1999-03-17 qualify Theory.sign_of etc.;
1998-12-28 paulson 1998-12-28 Added a "message" argument to print_tac
1998-11-30 paulson 1998-11-30 tactical CHANGED now uses alpha-eta conversion, not alpha conversion Streamlined code
1998-11-25 wenzelm 1998-11-25 tuned space;
1998-11-25 wenzelm 1998-11-25 replaced prs by writeln;
1998-11-17 wenzelm 1998-11-17 Drule.rev_triv_goal;
1998-08-13 paulson 1998-08-13 simpler SELECT_GOAL no longer inserts a dummy parameter
1998-07-14 paulson 1998-07-14 CHANGED_GOAL added to declare a more robust stac
1998-02-05 wenzelm 1998-02-05 added THEN_ALL_NEW;
1997-11-21 wenzelm 1997-11-21 changed Sequence interface (now Seq, in seq.ML);
1997-10-24 wenzelm 1997-10-24 ProtoPure.thy;