| 2007-09-18 | wenzelm | 2007-09-18 | simplified type int (eliminated IntInf.int, integer); | file | diff | annotate |
| 2007-08-14 | nipkow | 2007-08-14 | extended linear arith capabilities with code by Amine | file | diff | annotate |
| 2007-08-09 | haftmann | 2007-08-09 | localized of_nat | file | diff | annotate |
| 2007-07-31 | wenzelm | 2007-07-31 | tuned LinArith setup; | file | diff | annotate |
| 2007-07-31 | wenzelm | 2007-07-31 | arith method setup: proper context; | file | diff | annotate |
| 2007-07-20 | haftmann | 2007-07-20 | moved class ord from Orderings.thy to HOL.thy | file | diff | annotate |
| 2007-06-16 | nipkow | 2007-06-16 | The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no longer need class numeral_ring. This made a number of special simp-thms redundant. | file | diff | annotate |
| 2007-06-13 | huffman | 2007-06-13 | removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int | file | diff | annotate |
| 2007-05-31 | wenzelm | 2007-05-31 | moved Integ files to canonical place; | file | diff | annotate |