src/HOL/Integ/Integ.ML
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-27 nipkow 1998-04-27 Renamed expand_const -> split_const.
1998-04-21 oheimb 1998-04-21 made proof of zmult_congruent2 more stable
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-03 paulson 1998-03-03 Better simplification allows deletion of parts of proofs
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-23 paulson 1997-12-23 Decremented subscript because of change to iffD1
1997-12-05 wenzelm 1997-12-05 adapted proofs to cope with simprocs nat_cancel (by Stefan Berghofer);
1997-11-10 wenzelm 1997-11-10 ASCII-fied;
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-09-29 paulson 1997-09-29 result() -> qed
1997-02-25 pusch 1997-02-25 minor changes due to primrec defintions for +,-,*
1997-02-07 nipkow 1997-02-07 Modified proofs because of added "triv_forall_equality".
1996-11-26 paulson 1996-11-26 New material from Norbert Voelker for efficient binary comparisons
1996-11-21 paulson 1996-11-21 Tidied up some proofs, ...
1996-10-10 paulson 1996-10-10 Tidied some proofs: changed needed for de Morgan laws
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-07-30 berghofe 1996-07-30 Classical tactics now use default claset.
1996-06-14 paulson 1996-06-14 Explicitly included add_mult_distrib & add_mult_distrib2
1996-03-27 paulson 1996-03-27 Now use _irrefl instead of _anti_refl
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-10-04 clasohm 1995-10-04 added local simpsets
1995-03-24 clasohm 1995-03-24 changed syntax of tuples from <..., ...> to (..., ...)
1995-03-03 clasohm 1995-03-03 new version of HOL/Integ with curried function application