src/HOL/IOA/Solve.ML
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-07-12 wenzelm 1998-07-12 isatool expandshort;
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-27 oheimb 1998-04-27 cleanup for split_all_tac as wrapper in claset()
1998-04-27 nipkow 1998-04-27 Renamed expand_const -> split_const.
1998-04-24 oheimb 1998-04-24 improved split_all_tac significantly
1998-04-07 oheimb 1998-04-07 made split_all_tac as safe wrapper more defensive: if it is added as unsafe wrapper again (as its was before), this does not break the current proofs.
1998-04-02 oheimb 1998-04-02 split_all_tac now fails if there is nothing to split split_all_tac has moved within claset() from usafe wrappers to safe wrappers
1998-03-06 nipkow 1998-03-06 expand_if is now by default part of the simpset.
1998-02-25 oheimb 1998-02-25 changed wrapper mechanism of classical reasoner
1998-01-08 oheimb 1998-01-08 corrected Title
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-03 nipkow 1997-11-03 expand_option_case -> split_option_case
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-04-30 mueller 1997-04-30 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);