| Tue, 08 Mar 2016 21:07:48 +0100 |
haftmann |
explicit record values for dictionary variables
|
changeset |
files
|
| Tue, 08 Mar 2016 21:07:47 +0100 |
haftmann |
provide explicit hint concering uniqueness of derivation
|
changeset |
files
|
| Tue, 08 Mar 2016 21:07:46 +0100 |
haftmann |
syntax for multiset membership modelled after syntax for set membership
|
changeset |
files
|
| Mon, 07 Mar 2016 23:20:11 +0100 |
blanchet |
made 'size' plugin compatible with locales again (and added regression test)
|
changeset |
files
|
| Mon, 07 Mar 2016 23:20:11 +0100 |
blanchet |
strengthened tactic
|
changeset |
files
|
| Mon, 07 Mar 2016 15:57:02 +0000 |
paulson |
complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
|
changeset |
files
|
| Mon, 07 Mar 2016 14:34:45 +0000 |
paulson |
new material to Blochj's theorem, as well as supporting lemmas
|
changeset |
files
|
| Mon, 07 Mar 2016 08:14:18 +0100 |
traytel |
merged
|
changeset |
files
|
| Sun, 06 Mar 2016 20:39:19 +0100 |
traytel |
less resetting of local theories
|
changeset |
files
|
| Sun, 06 Mar 2016 18:15:09 +0100 |
wenzelm |
avoid redundant escapes;
|
changeset |
files
|
| Sun, 06 Mar 2016 16:19:02 +0100 |
wenzelm |
clarified treatment of fragments of Isabelle symbols during bootstrap;
|
changeset |
files
|
| Sun, 06 Mar 2016 13:19:19 +0100 |
wenzelm |
clarified ML syntax for strings concerning UTF8;
|
changeset |
files
|
| Sun, 06 Mar 2016 11:59:35 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 06 Mar 2016 10:33:34 +0100 |
nipkow |
tuned
|
changeset |
files
|