src/Pure/tctical.ML
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;
1997-09-11 wenzelm 1997-09-11 removed print_goals_ref (which was broken anyway);
1997-07-23 paulson 1997-07-23 Removal of tactical STATE
1997-03-18 paulson 1997-03-18 A more explicit prefix because gensym now generates easily predicatable identifiers
1997-02-21 paulson 1997-02-21 Replaced "flat" by the Basis Library function List.concat
1997-02-15 oheimb 1997-02-15 added THEN_MAYBE and THEN_MAYBE'
1997-02-04 paulson 1997-02-04 Gradual switching to Basis Library functions nth, drop, etc.
1996-11-27 paulson 1996-11-27 Converted I/O operatios for Basis Library compatibility
1996-11-04 paulson 1996-11-04 Renamed SELECT_GOAL's new parameter from x to selct to avoid clashes
1996-09-23 paulson 1996-09-23 Optimized version of SELECT_GOAL, up to 10% faster
1996-04-04 paulson 1996-04-04 Fixed error in CHANGED (caused by variable renaming)
1996-03-15 paulson 1996-03-15 Search tacticals moved to search.ML
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 inserted tabs again
1996-01-29 clasohm 1996-01-29 removed tabs
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1994-11-22 lcp 1994-11-22 Pure/tctical/protect_subgoal: simplified to use Sequence.hd Pure/tctical/DEPTH_FIRST: now suppresses duplicate solutions
1994-11-14 lcp 1994-11-14 Pure/tctical/select: now uses cprems_of instead of prems_of and cterm_of: new SELECT_GOAL is MUCH faster
1994-11-11 lcp 1994-11-11 Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST, REPEAT_DETERM_SOME: new
1994-10-31 lcp 1994-10-31 Pure/tctical/THEN_ELSE: new
1994-10-12 lcp 1994-10-12 Pure/tctical/suppress_tracing: new; can now switch tracing off until the next tactical call. There is no good way of doing this because of backtracking. Pure/tctical/exec_trace_command,tracify,traced_tac: these set, test and reset suppress_tracing
1994-01-18 lcp 1994-01-18 Many other files modified as follows: s|Sign.cterm|cterm|g s|Sign.ctyp|ctyp|g s|Sign.rep_cterm|rep_cterm|g s|Sign.rep_ctyp|rep_ctyp|g s|Sign.pprint_cterm|pprint_cterm|g s|Sign.pprint_ctyp|pprint_ctyp|g s|Sign.string_of_cterm|string_of_cterm|g s|Sign.string_of_ctyp|string_of_ctyp|g s|Sign.term_of|term_of|g s|Sign.typ_of|typ_of|g s|Sign.read_cterm|read_cterm|g s|Sign.read_insts|read_insts|g s|Sign.cfun|cterm_fun|g
1993-10-21 lcp 1993-10-21 Pure/drule/print_goals_ref: new, for Centaur interface Pure/tctical/tracify,print_tac: now call !print_goals_ref Pure/goals/print_top,prepare_proof: now call !print_goals_ref
1993-10-06 lcp 1993-10-06 tctical/dummy_quant_rl: specifies type prop to avoid the type variable ?'a from occurring -- which sometimes caused SELECT_GOAL to fail
1993-09-16 clasohm 1993-09-16 Initial revision