Sun, 24 Mar 2024 14:50:47 +0100 |
nipkow |
more uniform command names
|
file |
diff |
annotate
|
Mon, 19 Feb 2024 08:23:23 +0100 |
nipkow |
use define_time_fun
|
file |
diff |
annotate
|
Wed, 06 Dec 2023 12:06:29 +0100 |
nipkow |
tuned T functions: now 0 if not recursive
|
file |
diff |
annotate
|
Mon, 25 Jul 2022 12:19:59 +0200 |
nipkow |
replaced complicated lemma by a simpler one
|
file |
diff |
annotate
|
Fri, 15 Jul 2022 08:46:04 +0200 |
nipkow |
tuned names
|
file |
diff |
annotate
|
Tue, 05 Jan 2021 11:24:35 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Thu, 17 Dec 2020 13:51:22 +0000 |
Peter Lammich |
tuned running time functions
|
file |
diff |
annotate
|
Wed, 16 Dec 2020 17:47:50 +0000 |
Peter Lammich |
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
|
file |
diff |
annotate
|
Wed, 16 Dec 2020 16:53:13 +0000 |
Peter Lammich |
added missing +1 to T_insert (for function call)
|
file |
diff |
annotate
|
Tue, 15 Dec 2020 17:22:27 +0000 |
Peter Lammich |
removed redundant T_xxx_bound_aux lemmas
|
file |
diff |
annotate
|
Fri, 04 Dec 2020 17:54:57 +0000 |
Peter Lammich |
removed session name
|
file |
diff |
annotate
|
Fri, 04 Dec 2020 17:20:41 +0000 |
Peter Lammich |
summarized structural and ordering invariant for trees
|
file |
diff |
annotate
|
Thu, 26 Nov 2020 15:51:20 +0000 |
Peter Lammich |
renaming
|
file |
diff |
annotate
|
Fri, 06 Nov 2020 12:59:38 +0100 |
blanchet |
undid renaming accident
|
file |
diff |
annotate
|
Fri, 06 Nov 2020 12:48:31 +0100 |
blanchet |
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
|
file |
diff |
annotate
|
Fri, 23 Aug 2019 21:08:27 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
Wed, 31 Jul 2019 09:04:00 +0200 |
nipkow |
reduced dependencies
|
file |
diff |
annotate
|
Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
Mon, 25 Jun 2018 14:45:05 +0200 |
nipkow |
added lemmas; uniform names
|
file |
diff |
annotate
|
Tue, 08 May 2018 10:14:36 +0200 |
nipkow |
new def of sorted and sorted_wrt
|
file |
diff |
annotate
|
Sat, 21 Apr 2018 11:13:35 +0200 |
nipkow |
dont rename PQ.del_min
|
file |
diff |
annotate
|
Sat, 21 Apr 2018 08:41:42 +0200 |
nipkow |
del_min -> split_min
|
file |
diff |
annotate
|
Mon, 22 Jan 2018 15:50:29 +0100 |
Lars Hupel |
tuned
|
file |
diff |
annotate
|
Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
Thu, 31 Aug 2017 08:39:42 +0200 |
nipkow |
added PQ with merge
|
file |
diff |
annotate
|
Tue, 29 Aug 2017 17:01:11 +0200 |
nipkow |
tuned names
|
file |
diff |
annotate
|
Tue, 29 Aug 2017 16:54:54 +0200 |
nipkow |
simpler definition
|
file |
diff |
annotate
|
Tue, 29 Aug 2017 15:37:02 +0200 |
nipkow |
typo
|
file |
diff |
annotate
|
Tue, 29 Aug 2017 15:07:15 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
Sun, 27 Aug 2017 16:56:25 +0200 |
nipkow |
tuning
|
file |
diff |
annotate
|
Wed, 23 Aug 2017 20:41:15 +0200 |
nipkow |
reorg
|
file |
diff |
annotate
|
Tue, 15 Aug 2017 19:47:08 +0200 |
nipkow |
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
|
file |
diff |
annotate
|