| Mon, 07 Dec 2020 22:28:41 +0100 |
wenzelm |
spelling;
|
file |
diff |
annotate
|
| Sun, 06 Dec 2020 13:49:25 +0100 |
wenzelm |
more Unicode;
|
file |
diff |
annotate
|
| Sun, 06 Dec 2020 13:44:07 +0100 |
wenzelm |
eliminated odd "Read_me";
|
file |
diff |
annotate
|
| Sun, 06 Dec 2020 13:31:42 +0100 |
wenzelm |
eliminated odd "Read_me";
|
file |
diff |
annotate
|
| Mon, 23 Nov 2020 19:57:55 +0100 |
nipkow |
proper defn of a heap
|
file |
diff |
annotate
|
| Mon, 16 Nov 2020 22:21:40 +0100 |
wenzelm |
clarified document;
|
file |
diff |
annotate
|
| Sat, 14 Nov 2020 12:57:28 +0100 |
wenzelm |
proper document_theories;
|
file |
diff |
annotate
|
| Sun, 01 Nov 2020 16:54:49 +0100 |
haftmann |
bundle mixins for locale and class specifications
|
file |
diff |
annotate
|
| Thu, 29 Oct 2020 10:03:03 +0000 |
haftmann |
moved most material from session HOL-Word to Word_Lib in the AFP
|
file |
diff |
annotate
|
| Fri, 16 Oct 2020 19:34:37 +0200 |
Mathias Fleury |
reactivate veriT after changing options in 11f645d25498
|
file |
diff |
annotate
|
| Thu, 15 Oct 2020 13:24:16 +0200 |
wenzelm |
proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 18:59:44 +0200 |
Mathias Fleury |
add reconstruction for the SMT solver veriT
|
file |
diff |
annotate
|
| Wed, 07 Oct 2020 17:34:24 +0200 |
nipkow |
Aded Queues
|
file |
diff |
annotate
|
| Tue, 29 Sep 2020 12:12:34 +0200 |
wenzelm |
clarified default (see also 0c7a74a1c6d9);
|
file |
diff |
annotate
|
| Sat, 26 Sep 2020 17:04:51 +0200 |
wenzelm |
less bulky session stack;
|
file |
diff |
annotate
|
| Thu, 17 Sep 2020 09:57:31 +0000 |
haftmann |
integrated generic conversions into word corpse
|
file |
diff |
annotate
|
| Tue, 25 Aug 2020 15:02:56 +0200 |
wenzelm |
test HOL-Nitpick_Examples with Isabelle/Scala instead of external process: much faster;
|
file |
diff |
annotate
|
| Mon, 24 Aug 2020 13:39:09 +0000 |
haftmann |
a proof of concept for generic conversions
|
file |
diff |
annotate
|
| Sat, 22 Aug 2020 13:55:42 +0200 |
wenzelm |
clarified session: no parent image for minor theory imports;
|
file |
diff |
annotate
|
| Thu, 06 Aug 2020 15:37:14 +0000 |
haftmann |
tailored towards remaining essence
|
file |
diff |
annotate
|
| Thu, 06 Aug 2020 17:11:33 +0200 |
nipkow |
added theory Tree23_of_List
|
file |
diff |
annotate
|
| Fri, 17 Jul 2020 17:06:54 +0200 |
wenzelm |
proper session imports;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2020 16:53:08 +0200 |
wenzelm |
proper import sessions;
|
file |
diff |
annotate
|
| Mon, 13 Jul 2020 17:08:45 +0200 |
wenzelm |
clarified examples;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2020 12:10:58 +0000 |
haftmann |
extraction of equations x = t from premises beneath meta-all
|
file |
diff |
annotate
|
| Tue, 09 Jun 2020 12:13:15 +0100 |
paulson |
New Ackermann development
|
file |
diff |
annotate
|
| Mon, 08 Jun 2020 21:55:14 +0200 |
wenzelm |
clarified sessions;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2020 21:38:41 +0200 |
wenzelm |
clarified sessions: "Notable Examples in Isabelle/HOL";
|
file |
diff |
annotate
|
| Mon, 08 Jun 2020 15:09:57 +0200 |
wenzelm |
clarified sessions: "Notable Examples in Isabelle/Pure";
|
file |
diff |
annotate
|
| Sun, 17 May 2020 17:18:32 +0200 |
nipkow |
another AVL tree version
|
file |
diff |
annotate
|