| 2006-11-08 |
wenzelm |
2006-11-08 |
proper definition of add_zero_left/right;
|
file | diff | annotate |
| 2006-06-06 |
wenzelm |
2006-06-06 |
tuned;
|
file | diff | annotate |
| 2006-05-01 |
paulson |
2006-05-01 |
some facts about min, max and add, diff
|
file | diff | annotate |
| 2006-04-10 |
obua |
2006-04-10 |
Moved stuff from Ring_and_Field to Matrix
|
file | diff | annotate |
| 2006-03-10 |
haftmann |
2006-03-10 |
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
|
file | diff | annotate |
| 2005-08-16 |
paulson |
2005-08-16 |
more simprules now have names
|
file | diff | annotate |
| 2005-07-12 |
avigad |
2005-07-12 |
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.)
renamed simplification rules for abs (abs_of_pos, etc.)
renamed rules for multiplication and signs (mult_pos_pos, etc.)
moved lemmas involving fractions from NatSimprocs.thy
added setsum_mono3 to FiniteSet.thy
added simplification rules for powers to Parity.thy
|
file | diff | annotate |
| 2005-06-17 |
haftmann |
2005-06-17 |
migrated theory headers to new format
|
file | diff | annotate |
| 2005-03-07 |
obua |
2005-03-07 |
Cleaning up HOL/Matrix
|
file | diff | annotate |
| 2005-02-21 |
nipkow |
2005-02-21 |
comprehensive cleanup, replacing sumr by setsum
|
file | diff | annotate |
| 2005-02-01 |
paulson |
2005-02-01 |
the new subst tactic, by Lucas Dixon
|
file | diff | annotate |
| 2004-10-07 |
paulson |
2004-10-07 |
simplification tweaks for better arithmetic reasoning
|
file | diff | annotate |
| 2004-10-05 |
paulson |
2004-10-05 |
new simprules for abs and for things like a/b<1
|
file | diff | annotate |
| 2004-09-10 |
nipkow |
2004-09-10 |
Added antisymmetry simproc
|
file | diff | annotate |
| 2004-09-03 |
obua |
2004-09-03 |
Matrix theory, linear programming
|
file | diff | annotate |
| 2004-08-18 |
nipkow |
2004-08-18 |
import -> imports
|
file | diff | annotate |
| 2004-08-16 |
nipkow |
2004-08-16 |
New theory header syntax.
|
file | diff | annotate |
| 2004-07-30 |
paulson |
2004-07-30 |
conversion of Integration and NSPrimes to Isar scripts
|
file | diff | annotate |
| 2004-06-29 |
kleing |
2004-06-29 |
license change to BSD
|
file | diff | annotate |
| 2004-05-21 |
wenzelm |
2004-05-21 |
removed duplicate thms;
|
file | diff | annotate |
| 2004-05-18 |
obua |
2004-05-18 |
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
|
file | diff | annotate |
| 2004-05-11 |
obua |
2004-05-11 |
changes made due to new Ring_and_Field theory
|
file | diff | annotate |