| 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
|
| Mon, 04 May 2020 17:35:29 +0200 |
Manuel Eberl |
New HOL simproc 'datatype_no_proper_subterm'
|
file |
diff |
annotate
|
| Tue, 12 May 2020 16:29:26 +0200 |
wenzelm |
clarified session imports: avoid bulky HOL-Library image;
|
file |
diff |
annotate
|
| Mon, 04 May 2020 16:28:39 +0200 |
nipkow |
AVL trees with balance tags
|
file |
diff |
annotate
|
| Sat, 25 Apr 2020 16:31:43 +0200 |
nipkow |
added Height_Balanced_Trees
|
file |
diff |
annotate
|
| Fri, 17 Apr 2020 20:55:53 +0100 |
paulson |
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
|
file |
diff |
annotate
|
| Tue, 03 Mar 2020 19:26:24 +0000 |
haftmann |
library theory for extractions of equations x = t into premises
|
file |
diff |
annotate
|
| Fri, 28 Feb 2020 21:23:11 +0100 |
traytel |
tuned lift_bnf's user interface for quotients
|
file |
diff |
annotate
|
| Mon, 03 Feb 2020 16:49:44 +0100 |
nipkow |
added Interval_Tree.thy
|
file |
diff |
annotate
|
| Sun, 19 Jan 2020 07:50:35 +0100 |
traytel |
new examples of BNF lifting across quotients using a new theory of confluence,
|
file |
diff |
annotate
|
| Tue, 07 Jan 2020 12:37:12 +0100 |
nipkow |
alternative deletion in Red-Black trees
|
file |
diff |
annotate
|
| Tue, 10 Dec 2019 01:06:39 +0100 |
traytel |
an extensive example for lift_bnf across quotients
|
file |
diff |
annotate
|
| Sat, 30 Nov 2019 13:47:33 +0100 |
Manuel Eberl |
Split off new HOL-Complex_Analysis session from HOL-Analysis
|
file |
diff |
annotate
|
| Mon, 04 Nov 2019 20:38:15 +0000 |
haftmann |
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
|
file |
diff |
annotate
|
| Sun, 27 Oct 2019 20:53:10 -0400 |
immler |
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
|
file |
diff |
annotate
|
| Sun, 27 Oct 2019 20:07:59 -0400 |
immler |
added examples for "metric" method, by Maximilian Schäffeler
|
file |
diff |
annotate
|
| Sun, 13 Oct 2019 16:26:31 +0200 |
wenzelm |
clarified sessions/directories;
|
file |
diff |
annotate
|
| Mon, 07 Oct 2019 11:35:43 +0200 |
wenzelm |
discontinued pointless dump_checkpoint and share_common_data -- superseded by base logic image in Isabelle/MMT;
|
file |
diff |
annotate
|
| Wed, 02 Oct 2019 20:58:09 +0200 |
wenzelm |
just one dump_checkpoint Main -- potentially more robust;
|
file |
diff |
annotate
|
| Sun, 08 Sep 2019 17:49:35 +0200 |
wenzelm |
clarified syntax: 'directories' and 'theories' belong together;
|
file |
diff |
annotate
|
| Sun, 08 Sep 2019 16:49:05 +0200 |
wenzelm |
declare session directories;
|
file |
diff |
annotate
|
| Sat, 07 Sep 2019 12:16:11 +0200 |
wenzelm |
avoid overlapping session directories;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2019 15:50:57 +0200 |
wenzelm |
proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);
|
file |
diff |
annotate
|