| Fri, 08 Dec 2017 17:57:29 +0100 |
wenzelm |
clarified error;
|
changeset |
files
|
| Fri, 08 Dec 2017 16:02:44 +0100 |
wenzelm |
removed somewhat pointless warning;
|
changeset |
files
|
| Fri, 08 Dec 2017 15:03:54 +0100 |
wenzelm |
uniform use of original theory;
|
changeset |
files
|
| Fri, 08 Dec 2017 14:39:52 +0100 |
wenzelm |
implicit quick_and_dirty as for Toplevel.begin_proof/Proof.global_skip_proof;
|
changeset |
files
|
| Thu, 07 Dec 2017 18:44:04 +0000 |
haftmann |
avoid smt proofs in distribution
|
changeset |
files
|
| Thu, 07 Dec 2017 20:55:03 +0100 |
wenzelm |
more robust;
|
changeset |
files
|
| Thu, 07 Dec 2017 20:05:08 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 07 Dec 2017 19:36:48 +0100 |
wenzelm |
clarified document preparation vs. skip_proofs;
|
changeset |
files
|
| Thu, 07 Dec 2017 18:04:52 +0100 |
nipkow |
"important" annotations
|
changeset |
files
|
| Thu, 07 Dec 2017 15:48:50 +0100 |
nipkow |
canonical name
|
changeset |
files
|
| Thu, 07 Dec 2017 11:14:32 +0100 |
wenzelm |
tuned output in isar-ref manual;
|
changeset |
files
|
| Thu, 07 Dec 2017 11:12:55 +0100 |
wenzelm |
obsolete (used to be part of old src/Pure/codegen.ML);
|
changeset |
files
|