| Mon, 04 Aug 2008 18:56:22 +0200 |
berghofe |
- corrected bogus comment for function inst_conj_all
|
changeset |
files
|
| Mon, 04 Aug 2008 18:24:27 +0200 |
krauss |
removed dead code
|
changeset |
files
|
| Mon, 04 Aug 2008 17:13:34 +0200 |
wenzelm |
simplified prepare_command;
|
changeset |
files
|
| Mon, 04 Aug 2008 17:13:33 +0200 |
wenzelm |
Isar.command: explicitly set transaction position, as required for prepare_command errors;
|
changeset |
files
|
| Mon, 04 Aug 2008 10:37:33 +0200 |
ballarin |
Updated locale tests.
|
changeset |
files
|
| Fri, 01 Aug 2008 18:10:52 +0200 |
ballarin |
Generalised polynomial lemmas from cring to ring.
|
changeset |
files
|
| Fri, 01 Aug 2008 17:41:37 +0200 |
ballarin |
Removed import and lparams from locale record.
|
changeset |
files
|
| Fri, 01 Aug 2008 12:57:50 +0200 |
nipkow |
made setsum executable on int.
|
changeset |
files
|
| Thu, 31 Jul 2008 09:49:21 +0200 |
ballarin |
Tuned (for the sake of a meaningless log entry).
|
changeset |
files
|
| Wed, 30 Jul 2008 19:03:33 +0200 |
ballarin |
New locales for orders and lattices where the equivalence relation is not restricted to equality.
|
changeset |
files
|
| Wed, 30 Jul 2008 16:07:00 +0200 |
nipkow |
added hint about writing "x : set xs".
|
changeset |
files
|
| Wed, 30 Jul 2008 07:34:01 +0200 |
haftmann |
simple lifters
|
changeset |
files
|
| Wed, 30 Jul 2008 07:34:00 +0200 |
haftmann |
dropped imperative monad bind
|
changeset |
files
|
| Wed, 30 Jul 2008 07:33:59 +0200 |
haftmann |
facts_of
|
changeset |
files
|
| Wed, 30 Jul 2008 07:33:58 +0200 |
haftmann |
improved morphism
|
changeset |
files
|
| Wed, 30 Jul 2008 07:33:57 +0200 |
haftmann |
SML_imp, OCaml_imp
|
changeset |
files
|
| Wed, 30 Jul 2008 07:33:56 +0200 |
haftmann |
clarified
|
changeset |
files
|
| Wed, 30 Jul 2008 07:33:55 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Tue, 29 Jul 2008 17:50:48 +0200 |
ballarin |
Zorn's Lemma for partial orders.
|
changeset |
files
|
| Tue, 29 Jul 2008 17:50:12 +0200 |
ballarin |
Definitions and some lemmas for reflexive orderings.
|
changeset |
files
|
| Tue, 29 Jul 2008 17:49:26 +0200 |
ballarin |
Lemmas added
|
changeset |
files
|
| Tue, 29 Jul 2008 16:19:49 +0200 |
ballarin |
New theory on divisibility.
|
changeset |
files
|
| Tue, 29 Jul 2008 16:19:19 +0200 |
ballarin |
Renamed theorems;
|
changeset |
files
|
| Tue, 29 Jul 2008 16:17:45 +0200 |
ballarin |
New theorems on summation.
|
changeset |
files
|
| Tue, 29 Jul 2008 16:17:13 +0200 |
ballarin |
Unit_inv_l, Unit_inv_r made [simp].
|
changeset |
files
|
| Tue, 29 Jul 2008 16:16:10 +0200 |
ballarin |
New theory on divisibility;
|
changeset |
files
|
| Tue, 29 Jul 2008 16:14:56 +0200 |
ballarin |
Unit_inv_l, Unit_inv_r made [simp];
|
changeset |
files
|
| Tue, 29 Jul 2008 14:20:22 +0200 |
haftmann |
Haskell now living in the RealWorld
|
changeset |
files
|
| Tue, 29 Jul 2008 14:07:23 +0200 |
haftmann |
corrected Pure dependency
|
changeset |
files
|
| Tue, 29 Jul 2008 13:16:54 +0200 |
nipkow |
added removeAll
|
changeset |
files
|