Sat, 23 Jul 2016 13:25:44 +0200 |
nipkow |
added new vcg based on existentially quantified while-rule
|
file |
diff |
annotate
|
Fri, 22 Jul 2016 17:35:54 +0200 |
eberlm |
Removed redundant material related to primes
|
file |
diff |
annotate
|
Wed, 13 Jul 2016 15:46:52 +0200 |
eberlm |
Reformed factorial rings
|
file |
diff |
annotate
|
Mon, 04 Jul 2016 19:46:20 +0200 |
haftmann |
basic facts about almost everywhere fix bijections
|
file |
diff |
annotate
|
Fri, 10 Jun 2016 23:13:04 +0200 |
wenzelm |
bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;
|
file |
diff |
annotate
|
Tue, 31 May 2016 12:24:43 +0200 |
blanchet |
added test
|
file |
diff |
annotate
|
Thu, 26 May 2016 15:31:04 +0200 |
haftmann |
examples and documentation for code generator time measurements
|
file |
diff |
annotate
|
Fri, 13 May 2016 20:22:02 +0200 |
wenzelm |
more complete theories;
|
file |
diff |
annotate
|
Tue, 10 May 2016 14:04:44 +0100 |
paulson |
Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
|
file |
diff |
annotate
|
Sun, 01 May 2016 17:26:27 +0200 |
nipkow |
the standard While-rule
|
file |
diff |
annotate
|
Sun, 17 Apr 2016 16:02:44 +0200 |
Lars Hupel |
remove "slow" session tags
|
file |
diff |
annotate
|
Sun, 17 Apr 2016 12:59:55 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
Fri, 15 Apr 2016 18:05:57 +0200 |
Lars Hupel |
add "slow" group to descendants of HOL-Proofs
|
file |
diff |
annotate
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
another 'corec' example
|
file |
diff |
annotate
|
Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
new 'corec' example
|
file |
diff |
annotate
|
Thu, 24 Mar 2016 15:56:47 +0100 |
nipkow |
added Leftist_Heap
|
file |
diff |
annotate
|
Tue, 22 Mar 2016 12:39:37 +0100 |
blanchet |
added 'corec' examples and tests
|
file |
diff |
annotate
|
Tue, 22 Mar 2016 12:39:37 +0100 |
blanchet |
added two 'corec' examples
|
file |
diff |
annotate
|
Mon, 29 Feb 2016 22:34:36 +0100 |
wenzelm |
clarified session;
|
file |
diff |
annotate
|
Tue, 23 Feb 2016 15:37:18 +0100 |
nipkow |
was only of historical interest anymore
|
file |
diff |
annotate
|
Fri, 19 Feb 2016 15:01:38 +0100 |
wenzelm |
moved examples to avoid dependency on bulky HOL-Proofs session, e.g. relevant for "isabelle makedist";
|
file |
diff |
annotate
|
Wed, 17 Feb 2016 23:29:35 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
Wed, 17 Feb 2016 23:06:24 +0100 |
wenzelm |
SML/NJ is no longer supported;
|
file |
diff |
annotate
|
Wed, 17 Feb 2016 21:51:58 +0100 |
haftmann |
separated potentially conflicting type class instance into separate theory
|
file |
diff |
annotate
|
Sat, 13 Feb 2016 12:13:10 +0100 |
wenzelm |
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
|
file |
diff |
annotate
|
Sat, 13 Feb 2016 11:50:01 +0100 |
wenzelm |
unconditional test -- nothing special here;
|
file |
diff |
annotate
|
Sun, 24 Jan 2016 15:25:39 +0100 |
wenzelm |
guard sessions that no longer work with SML/NJ -- memory problems;
|
file |
diff |
annotate
|
Wed, 13 Jan 2016 16:41:32 +0100 |
wenzelm |
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
|
file |
diff |
annotate
|
Tue, 12 Jan 2016 20:05:53 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
Tue, 12 Jan 2016 14:41:35 +0100 |
wenzelm |
removed in anticipation of c92d82c3f41b -- demolition after renovation;
|
file |
diff |
annotate
|
Tue, 12 Jan 2016 09:28:08 +0100 |
traytel |
removed outdated example
|
file |
diff |
annotate
|
Mon, 11 Jan 2016 20:51:13 +0100 |
nipkow |
added AA_Map; tuned titles
|
file |
diff |
annotate
|
Thu, 31 Dec 2015 12:43:09 +0100 |
wenzelm |
clarified directory structure;
|
file |
diff |
annotate
|
Sun, 27 Dec 2015 17:08:31 +0100 |
haftmann |
put example into separate session, to restrict precious session image to library theories
|
file |
diff |
annotate
|
Sun, 27 Dec 2015 16:20:02 +0100 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
Sun, 27 Dec 2015 16:00:41 +0100 |
wenzelm |
more proofs;
|
file |
diff |
annotate
|
Sat, 26 Dec 2015 19:27:46 +0100 |
wenzelm |
clarified sessions;
|
file |
diff |
annotate
|
Sun, 06 Dec 2015 17:27:42 +0100 |
nipkow |
added AA trees
|
file |
diff |
annotate
|
Sat, 05 Dec 2015 16:13:28 +0100 |
nipkow |
added Brother12_Map
|
file |
diff |
annotate
|
Fri, 04 Dec 2015 14:39:31 +0100 |
nipkow |
added 1-2 brother trees
|
file |
diff |
annotate
|
Tue, 24 Nov 2015 10:54:21 +0100 |
traytel |
Ported old example to use (co)datatypes
|
file |
diff |
annotate
|
Sat, 14 Nov 2015 08:45:52 +0100 |
haftmann |
coalesce permanent_interpretation.ML with interpretation.ML
|
file |
diff |
annotate
|
Mon, 02 Nov 2015 14:09:14 +0100 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
Fri, 30 Oct 2015 20:01:05 +0100 |
nipkow |
added splay trees
|
file |
diff |
annotate
|
Sun, 25 Oct 2015 17:30:06 +0100 |
nipkow |
added 234-Trees (slow)
|
file |
diff |
annotate
|
Sun, 18 Oct 2015 17:25:13 +0200 |
nipkow |
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
|
file |
diff |
annotate
|
Fri, 09 Oct 2015 01:44:27 +0200 |
kuncar |
add a file with examples of debugging transfer
|
file |
diff |
annotate
|
Wed, 23 Sep 2015 09:47:04 +0200 |
nipkow |
added AVL and lookup function
|
file |
diff |
annotate
|
Tue, 22 Sep 2015 08:38:25 +0200 |
nipkow |
added red black trees
|
file |
diff |
annotate
|
Mon, 21 Sep 2015 14:44:32 +0200 |
nipkow |
New subdirectory for functional data structures
|
file |
diff |
annotate
|
Thu, 10 Sep 2015 16:42:01 +0200 |
wenzelm |
HOL-Proofs is slow;
|
file |
diff |
annotate
|
Wed, 09 Sep 2015 17:07:44 +0200 |
Andreas Lochbihler |
reactivate examples with predicate compiler and quickcheck
|
file |
diff |
annotate
|
Wed, 12 Aug 2015 20:46:33 +0200 |
traytel |
actually process lift_bnf regression suite
|
file |
diff |
annotate
|
Tue, 28 Jul 2015 16:16:13 +0100 |
paulson |
the Cauchy integral theorem and related material
|
file |
diff |
annotate
|
Mon, 27 Jul 2015 22:44:02 +0200 |
haftmann |
formal class for factorial (semi)rings
|
file |
diff |
annotate
|
Sat, 18 Jul 2015 20:37:16 +0200 |
wenzelm |
reactivated dead code;
|
file |
diff |
annotate
|
Fri, 12 Jun 2015 10:33:02 +0200 |
bulwahn |
add examples from Freek's top 100 theorems (thms 30, 73, 77)
|
file |
diff |
annotate
|
Sun, 14 Jun 2015 16:18:00 +0200 |
wenzelm |
more examples;
|
file |
diff |
annotate
|
Sat, 13 Jun 2015 13:18:37 +0200 |
wenzelm |
more examples;
|
file |
diff |
annotate
|
Mon, 01 Jun 2015 15:39:53 +0200 |
wenzelm |
discontinued unused / unmaintained SVC oracle -- current Isabelle tools (e.g. arith, smt) can easily solve the given examples with full proof reconstruction;
|
file |
diff |
annotate
|