| Mon, 27 Oct 2014 12:03:13 +0100 |
hoelzl |
generalize natfloor_div_nat, add floor variant: floor_divide_real_eq_div
|
changeset |
files
|
| Sun, 26 Oct 2014 19:11:16 +0100 |
haftmann |
eliminated redundancies;
|
changeset |
files
|
| Sat, 25 Oct 2014 19:20:28 +0200 |
haftmann |
more simp rules;
|
changeset |
files
|
| Sun, 26 Oct 2014 15:57:10 +0100 |
wenzelm |
clarified default;
|
changeset |
files
|
| Sun, 26 Oct 2014 15:46:02 +0100 |
wenzelm |
support negative extraLineSpacing;
|
changeset |
files
|
| Sat, 25 Oct 2014 21:16:32 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sat, 25 Oct 2014 11:53:35 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Fri, 24 Oct 2014 20:49:23 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Fri, 24 Oct 2014 11:30:39 +0200 |
wenzelm |
discontinued python from standard system environment;
|
changeset |
files
|
| Fri, 24 Oct 2014 11:05:19 +0200 |
wenzelm |
more generous default;
|
changeset |
files
|
| Thu, 23 Oct 2014 19:40:41 +0200 |
haftmann |
even further downshift of theory Parity in the hierarchy
|
changeset |
files
|
| Thu, 23 Oct 2014 19:40:39 +0200 |
haftmann |
further downshift of theory Parity in the hierarchy
|
changeset |
files
|
| Fri, 24 Oct 2014 15:07:51 +0200 |
hoelzl |
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
|
changeset |
files
|
| Fri, 24 Oct 2014 15:07:49 +0200 |
hoelzl |
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
|
changeset |
files
|