| 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
|
| Sat, 02 May 2015 13:58:06 +0200 |
kuncar |
add testing file for code_dt extension of lifting
|
file |
diff |
annotate
|
| Fri, 17 Apr 2015 17:49:19 +0200 |
wenzelm |
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
|
file |
diff |
annotate
|
| Sat, 11 Apr 2015 12:24:51 +0200 |
wenzelm |
make SML/NJ more happy;
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 22:53:26 +0200 |
wenzelm |
make SML/NJ more happy;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 20:41:56 +0200 |
wenzelm |
proper test for session HOL-Library;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2015 21:25:55 +0200 |
wenzelm |
rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 22:40:41 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 18:22:55 +0200 |
wenzelm |
clarified "main" group, e.g. relevant for Isabelle/jEdit menu;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 15:47:55 +0100 |
paulson |
John Harrison's example: a 32-bit approximation to pi. SLOW
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 13:31:47 +0100 |
wenzelm |
HOL-SPARK .prv files are subject to system option spark_prv;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 08:45:54 +0100 |
nipkow |
BT subsumed by Library/Tree
|
file |
diff |
annotate
|
| Wed, 18 Mar 2015 21:40:21 +0100 |
traytel |
bounded powerset
|
file |
diff |
annotate
|
| Wed, 18 Mar 2015 14:28:40 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
| Wed, 18 Mar 2015 14:13:27 +0000 |
paulson |
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
|
file |
diff |
annotate
|
| Wed, 18 Mar 2015 13:51:33 +0100 |
noschinl |
added proof method rewrite
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 15:20:40 +0000 |
paulson |
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 23:02:39 +0100 |
wenzelm |
check unused theory;
|
file |
diff |
annotate
|
| Sun, 25 Jan 2015 22:11:06 +0100 |
wenzelm |
discontinued obsolete option "document_graph";
|
file |
diff |
annotate
|
| Sun, 28 Dec 2014 15:42:34 +1100 |
kleing |
3 old example lemmas by Amine listed in the top 100 theorems
|
file |
diff |
annotate
|
| Sat, 20 Dec 2014 00:05:20 +0100 |
wenzelm |
afford full test, with slightly improved scheduling order;
|
file |
diff |
annotate
|
| Wed, 17 Dec 2014 16:10:30 +0100 |
hoelzl |
unfortunately, there is no general function space in the measurable spaces
|
file |
diff |
annotate
|
| Thu, 04 Dec 2014 20:56:38 +0100 |
wenzelm |
more examples;
|
file |
diff |
annotate
|
| Fri, 14 Nov 2014 21:36:50 +0100 |
wenzelm |
no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 18:56:59 +0100 |
wenzelm |
discontinued pointless option: timing is always on (overall theory only);
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:18:17 +0100 |
wenzelm |
discontinued Proof General;
|
file |
diff |
annotate
|
| Fri, 10 Oct 2014 18:23:59 +0200 |
nipkow |
New example Bubblesort
|
file |
diff |
annotate
|