src/HOL/Divides.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 Removal of leading "\!\!..." from most Goal commands
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-21 paulson 1998-04-21 Renamed mod_XXX_cancel to mod_XXX_self Included their div_ equivalents
1998-04-20 paulson 1998-04-20 New laws for mod
1998-04-03 paulson 1998-04-03 Tidied proofs by getting rid of case_tac
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-16 wenzelm 1997-12-16 expandshort;
1997-12-11 paulson 1997-12-11 Got rid of mod2_neq_0
1997-12-04 nipkow 1997-12-04 Added thm mult_div_cancel
1997-12-03 nipkow 1997-12-03 Replaced n ~= 0 by 0 < n
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-01 paulson 1997-11-01 New Blast_tac (and minor tidying...)
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-09-29 paulson 1997-09-29 Step_tac -> Safe_tac
1997-09-26 paulson 1997-09-26 Minor tidying to use Clarify_tac, etc.
1997-07-04 paulson 1997-07-04 Simplified the new proofs about division
1997-07-02 nipkow 1997-07-02 Added the following lemmas tp Divides and a few others to Arith and NatDef: div_le_mono, div_le_mono2, div_le_dividend, div_less_dividend Fixed a broken proof in WF_Rel.ML. No idea what caused this.
1997-06-23 paulson 1997-06-23 Ran expandshort
1997-06-06 paulson 1997-06-06 Removed a few redundant additions of simprules or classical rules
1997-05-30 paulson 1997-05-30 Moving div and mod from Arith to Divides Moving dvd from ex/Primes to Divides