| Mon, 19 Aug 2019 20:00:29 +0200 |
wenzelm |
back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;
|
changeset |
files
|
| Mon, 19 Aug 2019 19:31:31 +0200 |
wenzelm |
module Thm_Name for Isabelle/Scala;
|
changeset |
files
|
| Mon, 19 Aug 2019 19:24:18 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 19 Aug 2019 19:12:44 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Mon, 19 Aug 2019 18:47:49 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 19 Aug 2019 18:41:03 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Mon, 19 Aug 2019 16:49:24 +0200 |
nipkow |
tuned names
|
changeset |
files
|
| Sat, 17 Aug 2019 19:04:03 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 17 Aug 2019 17:59:55 +0200 |
wenzelm |
discontinued peek_status: unused and not clearly defined;
|
changeset |
files
|
| Sat, 17 Aug 2019 17:57:10 +0200 |
wenzelm |
more documentation on oracles;
|
changeset |
files
|
| Sat, 17 Aug 2019 17:45:04 +0200 |
wenzelm |
proper theory context for global props;
|
changeset |
files
|
| Sat, 17 Aug 2019 17:28:08 +0200 |
wenzelm |
more thorough check, using full dependency graph of finished proofs;
|
changeset |
files
|
| Sat, 17 Aug 2019 17:21:30 +0200 |
wenzelm |
added ML antiquotation @{oracle_name};
|
changeset |
files
|
| Sat, 17 Aug 2019 13:39:28 +0200 |
wenzelm |
more robust, notably for open_proof of unnamed derivation;
|
changeset |
files
|
| Sat, 17 Aug 2019 13:24:40 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|