| Sun, 03 Dec 2017 19:09:42 +0100 |
wenzelm |
simplified session (again, see 39e29972cb96): WordExamples requires < 1s;
|
file |
diff |
annotate
|
| Mon, 27 Nov 2017 16:18:29 +0100 |
wenzelm |
clarified main sessions;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2017 14:52:27 +0100 |
nipkow |
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
|
file |
diff |
annotate
|
| Fri, 03 Nov 2017 13:43:31 +0100 |
wenzelm |
less global theories -- avoid confusion about special cases;
|
file |
diff |
annotate
|
| Wed, 01 Nov 2017 22:13:38 +0100 |
wenzelm |
more timing;
|
file |
diff |
annotate
|
| Wed, 01 Nov 2017 18:37:49 +0100 |
wenzelm |
build faster without heap images for minor imports;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2017 15:13:08 +0100 |
wenzelm |
no censorship (in contrast to 2c828c830ad7);
|
file |
diff |
annotate
|
| Tue, 31 Oct 2017 07:11:03 +0000 |
haftmann |
removed ancient nat-int transfer
|
file |
diff |
annotate
|
| Mon, 30 Oct 2017 20:26:19 +0100 |
wenzelm |
recovered document from 9bfb6978eb80;
|
file |
diff |
annotate
|
| Mon, 30 Oct 2017 20:04:10 +0100 |
wenzelm |
ROOT cleanup: empty 'document_files' means there is no document;
|
file |
diff |
annotate
|
| Sat, 28 Oct 2017 21:26:51 +0200 |
wenzelm |
reduced heap hierarchy, for potentially improved performance;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2017 20:46:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
Polynomial_Factorial does not depend on Field_as_Ring as such
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:19 +0200 |
haftmann |
removed mere toy example from library
|
file |
diff |
annotate
|
| Sat, 07 Oct 2017 20:20:03 +0200 |
wenzelm |
clarified session structure;
|
file |
diff |
annotate
|
| Mon, 02 Oct 2017 19:38:39 +0200 |
wenzelm |
prefer file dependencies wrt. specific theories;
|
file |
diff |
annotate
|
| Mon, 02 Oct 2017 18:35:51 +0200 |
wenzelm |
proper document (cf. 9f5bfef8bd82);
|
file |
diff |
annotate
|
| Mon, 02 Oct 2017 18:11:28 +0200 |
wenzelm |
removed pointless dependencies: done by 'spark_open';
|
file |
diff |
annotate
|
| Mon, 02 Oct 2017 16:41:59 +0200 |
wenzelm |
clarified imports: prefer parent session images;
|
file |
diff |
annotate
|
| Mon, 02 Oct 2017 16:08:43 +0200 |
wenzelm |
eliminated old-style no-document imports;
|
file |
diff |
annotate
|
| Fri, 08 Sep 2017 02:22:58 +0200 |
blanchet |
removed obsolete session
|
file |
diff |
annotate
|
| Thu, 31 Aug 2017 14:32:23 +0200 |
nipkow |
Moved material into AFP/Splay_Tree
|
file |
diff |
annotate
|
| Tue, 29 Aug 2017 12:05:00 +0200 |
nipkow |
new file
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Thu, 17 Aug 2017 14:40:42 +0200 |
wenzelm |
more complete session (amending e77ea0ea7f2c);
|
file |
diff |
annotate
|
| Thu, 17 Aug 2017 14:28:01 +0200 |
wenzelm |
clarified imports;
|
file |
diff |
annotate
|
| Thu, 17 Aug 2017 14:13:34 +0200 |
wenzelm |
more complete session (amending 783861a66a60);
|
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
|
| Tue, 11 Jul 2017 17:22:33 +0200 |
Lars Hupel |
State_Monad ~> Open_State_Syntax
|
file |
diff |
annotate
|
| Wed, 07 Jun 2017 20:18:23 +0200 |
wenzelm |
clarified imports;
|
file |
diff |
annotate
|
| Mon, 05 Jun 2017 15:59:45 +0200 |
haftmann |
specific output setup is not supposed to intrude regular import theory
|
file |
diff |
annotate
|
| Mon, 29 May 2017 09:14:15 +0200 |
eberlm |
reorganised material on sublists
|
file |
diff |
annotate
|
| Tue, 02 May 2017 10:47:39 +0200 |
wenzelm |
more timing;
|
file |
diff |
annotate
|
| Mon, 24 Apr 2017 23:10:01 +0200 |
wenzelm |
recovered document from 0f3fdf689bf9;
|
file |
diff |
annotate
|
| Mon, 24 Apr 2017 13:58:38 +0200 |
wenzelm |
clarified parent session images, to avoid duplicate loading of theories;
|
file |
diff |
annotate
|
| Mon, 24 Apr 2017 11:52:51 +0200 |
wenzelm |
clarified parent session images, to avoid duplicate loading of theories;
|
file |
diff |
annotate
|
| Sun, 23 Apr 2017 23:54:06 +0200 |
wenzelm |
actually use theory;
|
file |
diff |
annotate
|
| Sun, 23 Apr 2017 23:49:14 +0200 |
wenzelm |
clarified parent session images, to avoid duplicate loading of theories;
|
file |
diff |
annotate
|
| Sun, 23 Apr 2017 19:06:53 +0200 |
wenzelm |
actually use theory;
|
file |
diff |
annotate
|
| Sun, 23 Apr 2017 18:54:18 +0200 |
wenzelm |
renamed theory to avoid conflict with loaded theory "Tree" from HOL-Library;
|
file |
diff |
annotate
|
| Sat, 22 Apr 2017 22:01:35 +0200 |
wenzelm |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
|
file |
diff |
annotate
|
| Sat, 22 Apr 2017 12:52:16 +0200 |
wenzelm |
clarified parent session images, to avoid duplicate loading of theories;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 21:41:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 21:36:49 +0200 |
wenzelm |
removed pointless document;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 20:36:20 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 20:07:51 +0200 |
wenzelm |
clarified session imports;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 16:48:58 +0200 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 16:12:11 +0200 |
wenzelm |
clarified imports;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 11:38:45 +0200 |
wenzelm |
include imports that morally belong to Main and are used in HOL-Proofs applications;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2017 16:21:28 +0200 |
blanchet |
removed Old_SMT legacy module
|
file |
diff |
annotate
|
| Wed, 19 Apr 2017 15:53:58 +0200 |
wenzelm |
clarified session structure: avoid ambiguity of file ~~/src/HOL/Library/Old_Datatype.thy;
|
file |
diff |
annotate
|
| Mon, 17 Apr 2017 07:44:21 +0200 |
haftmann |
consistent session name
|
file |
diff |
annotate
|
| Tue, 11 Apr 2017 16:18:01 +0200 |
wenzelm |
less global theories -- conflict with AFP entries;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 13:30:55 +0200 |
wenzelm |
explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2017 20:17:00 +0200 |
wenzelm |
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
|
file |
diff |
annotate
|
| Thu, 06 Apr 2017 21:37:13 +0200 |
haftmann |
session containing computational algebra
|
file |
diff |
annotate
|
| Thu, 06 Apr 2017 08:33:37 +0200 |
haftmann |
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
|
file |
diff |
annotate
|
| Tue, 04 Apr 2017 22:16:42 +0200 |
wenzelm |
more main sessions and global theories;
|
file |
diff |
annotate
|
| Tue, 04 Apr 2017 22:07:34 +0200 |
wenzelm |
eliminated redundant imports;
|
file |
diff |
annotate
|
| Tue, 04 Apr 2017 21:57:43 +0200 |
wenzelm |
eliminated Plain_HOLCF.thy (see also 8e92772bc0e8): it was modeled after HOL/Plain.thy which was discontinued later;
|
file |
diff |
annotate
|
| Tue, 04 Apr 2017 21:11:40 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 04 Apr 2017 21:05:07 +0200 |
wenzelm |
tuned syntax;
|
file |
diff |
annotate
|
| Thu, 02 Mar 2017 21:16:02 +0100 |
ballarin |
Knaster-Tarski fixed point theorem and Galois Connections.
|
file |
diff |
annotate
|
| Sun, 26 Feb 2017 13:22:14 +0100 |
haftmann |
re-established AFP entry for FinFuns as library
|
file |
diff |
annotate
|
| Thu, 02 Feb 2017 14:42:06 +0100 |
blanchet |
added veriT preprocessing proof reconstruction example
|
file |
diff |
annotate
|
| Fri, 27 Jan 2017 22:27:03 +0100 |
haftmann |
ML antiquotation for generated computations
|
file |
diff |
annotate
|
| Wed, 18 Jan 2017 17:56:52 +0100 |
wenzelm |
clarified theory name;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2017 17:45:51 +0100 |
eberlm |
Added Circle_Area to HOL-Analysis examples
|
file |
diff |
annotate
|
| Sun, 18 Dec 2016 13:46:57 +0100 |
wenzelm |
test parallel proof terms in this small session (somewhat slow for bigger applications);
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:13 +0100 |
haftmann |
restructured matter on polynomials and normalized fractions
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:13 +0100 |
haftmann |
clarified library contents
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 14:47:41 +0100 |
wenzelm |
unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
|
file |
diff |
annotate
|
| Wed, 14 Dec 2016 18:37:54 +0100 |
wenzelm |
simplified options;
|
file |
diff |
annotate
|
| Mon, 12 Dec 2016 17:40:06 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 12 Dec 2016 11:33:14 +0100 |
wenzelm |
proper session HOL-Types_To_Sets;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2016 16:28:42 +0100 |
nipkow |
moved IMP/Abs_Int_ITP to AFP/Abs_Int_ITP2012
|
file |
diff |
annotate
|
| Sun, 30 Oct 2016 13:15:14 +0100 |
kuncar |
types to sets: initial commit
|
file |
diff |
annotate
|
| Mon, 24 Oct 2016 22:42:07 +0200 |
blanchet |
added Nunchaku integration
|
file |
diff |
annotate
|
| Mon, 24 Oct 2016 16:53:32 +0200 |
traytel |
additional user-specified simp (naturality) rules used in friend_of_corec
|
file |
diff |
annotate
|
| Thu, 20 Oct 2016 19:39:27 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 15:20:06 +0200 |
eberlm |
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
|
file |
diff |
annotate
|
| Mon, 03 Oct 2016 14:37:06 +0200 |
haftmann |
proof of concept for algebraically founded word types
|
file |
diff |
annotate
|
| Sat, 01 Oct 2016 17:38:14 +0200 |
wenzelm |
Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
|
file |
diff |
annotate
|
| Thu, 29 Sep 2016 20:54:44 +0200 |
boehmes |
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 23:14:34 +0200 |
kuncar |
resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
|
file |
diff |
annotate
|
| Fri, 16 Sep 2016 15:54:50 +0200 |
wenzelm |
sessions that are relevant for routine timing measurements;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 22:41:05 +0200 |
Lars Hupel |
new type for finite maps; use it in HOL-Probability
|
file |
diff |
annotate
|
| Fri, 09 Sep 2016 14:15:16 +0200 |
nipkow |
More on balancing; renamed theory to Balance
|
file |
diff |
annotate
|
| Thu, 08 Sep 2016 18:18:57 +0200 |
wenzelm |
option "checkpoint" helps to fine-tune global heap space management;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2016 21:28:46 +0200 |
wenzelm |
clarified session: use all theories in directory HOL/Library;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2016 12:10:52 +0200 |
blanchet |
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
|
file |
diff |
annotate
|
| Tue, 09 Aug 2016 21:18:32 +0200 |
nipkow |
New theory Balance_List
|
file |
diff |
annotate
|
| Mon, 08 Aug 2016 14:13:14 +0200 |
hoelzl |
rename HOL-Multivariate_Analysis to HOL-Analysis.
|
file |
diff |
annotate
|
| Thu, 04 Aug 2016 19:36:31 +0200 |
hoelzl |
HOL-Multivariate_Analysis: rename theories for more descriptive names
|
file |
diff |
annotate
|
| 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
|
| 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
|
| Wed, 08 Oct 2014 11:09:17 +0200 |
wenzelm |
simplified "sos" method;
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 09:09:12 +0200 |
Andreas Lochbihler |
move Code_Test to HOL/Library;
|
file |
diff |
annotate
|
| Tue, 07 Oct 2014 23:29:43 +0200 |
wenzelm |
more bibtex entries;
|
file |
diff |
annotate
|
| Wed, 24 Sep 2014 17:33:53 +0200 |
blanchet |
made N2M tests conditional, since they appear to cause Isatest timeouts and are kind of slow
|
file |
diff |
annotate
|
| Mon, 22 Sep 2014 21:45:59 +0200 |
wenzelm |
clarified timeout for isatest;
|
file |
diff |
annotate
|
| Mon, 22 Sep 2014 16:28:24 +0200 |
wenzelm |
examples for local CSDP executable;
|
file |
diff |
annotate
|
| Mon, 22 Sep 2014 16:15:29 +0200 |
wenzelm |
clarified SOS tool setup vs. examples;
|
file |
diff |
annotate
|
| Mon, 22 Sep 2014 10:18:41 +0200 |
wenzelm |
clarified ISABELLE_POLYML;
|
file |
diff |
annotate
|
| Sun, 21 Sep 2014 20:22:12 +0200 |
wenzelm |
renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
|
file |
diff |
annotate
|
| Fri, 19 Sep 2014 10:00:34 +0200 |
traytel |
regression tests for n2m
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
increased 'HOL-Proofs' timeout
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 00:03:46 +0200 |
blanchet |
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
|
file |
diff |
annotate
|
| Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
took out 'old_datatype' examples -- those just cause timeouts in Isatests
|
file |
diff |
annotate
|
| Fri, 12 Sep 2014 17:51:31 +0200 |
blanchet |
enabled 'Sudoku' only with 'ISABELLE_FULL_TEST' -- Sudoku is fast enough on modern hardware (within seconds on my MacBook), but it seems to fail on older test machines
|
file |
diff |
annotate
|
| Fri, 12 Sep 2014 16:42:36 +0200 |
blanchet |
run larger nominal examples only 'ISABELLE_FULL_TEST'
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:39:48 +0200 |
blanchet |
renamed example theory for consistency
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:38:22 +0200 |
blanchet |
updated ROOT
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:26:59 +0200 |
blanchet |
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:20:23 +0200 |
blanchet |
move datatype benchmarks
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
took out legacy material from 'HOL/Library/Library.thy'
|
file |
diff |
annotate
|
| Mon, 25 Aug 2014 09:40:50 +0200 |
Andreas Lochbihler |
add testing framework for generated code
|
file |
diff |
annotate
|
| Fri, 22 Aug 2014 08:43:14 +0200 |
haftmann |
generic euclidean algorithm (due to Manuel Eberl)
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 15:19:16 +0200 |
Andreas Lochbihler |
rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 09:36:37 +0200 |
blanchet |
avoid old 'smt' method in examples
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 14:04:55 +0200 |
wenzelm |
proper scope of comments;
|
file |
diff |
annotate
|
| Mon, 21 Jul 2014 18:04:08 +0200 |
traytel |
regression test for datatypes defined in IsaFoR
|
file |
diff |
annotate
|
| Sun, 20 Jul 2014 22:05:35 +0200 |
wenzelm |
proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
|
file |
diff |
annotate
|
| Fri, 11 Jul 2014 15:52:03 +0200 |
Andreas Lochbihler |
reactivate session Quickcheck_Examples
|
file |
diff |
annotate
|
| Fri, 11 Jul 2014 15:35:11 +0200 |
Andreas Lochbihler |
adapt and reactivate Quickcheck_Types and add two test cases
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 15:50:28 +0200 |
wenzelm |
revived unchecked theory (see cebaf814ca6e);
|
file |
diff |
annotate
|
| Sun, 29 Jun 2014 18:30:24 +0200 |
blanchet |
use SMT2
|
file |
diff |
annotate
|
| Thu, 22 May 2014 15:49:36 +0200 |
wenzelm |
include Nominal2 keywords -- Proof General legacy;
|
file |
diff |
annotate
|
| Mon, 19 May 2014 13:44:13 +0200 |
hoelzl |
fixed document generation for HOL-Probability
|
file |
diff |
annotate
|
| Mon, 12 May 2014 00:13:38 +0200 |
webertj |
Replaced refute with nitpick.
|
file |
diff |
annotate
|
| Fri, 09 May 2014 08:13:36 +0200 |
haftmann |
removed junk from library theory
|
file |
diff |
annotate
|
| Thu, 01 May 2014 22:57:38 +0200 |
boehmes |
use SMT2 for Boogie examples
|
file |
diff |
annotate
|
| Thu, 01 May 2014 22:56:59 +0200 |
boehmes |
added internal proof-producing SAT solver
|
file |
diff |
annotate
|
| Wed, 30 Apr 2014 22:34:11 +0200 |
wenzelm |
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
|
file |
diff |
annotate
|
| Tue, 29 Apr 2014 13:29:05 +0200 |
wenzelm |
systematic replacement of 'files' by 'document_files';
|
file |
diff |
annotate
|
| Thu, 24 Apr 2014 10:33:17 +0200 |
haftmann |
now covered by AFP 3ddac3e572cf
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 17:57:56 +0200 |
kuncar |
all BNF tests can be part of a normal session because they are much faster now
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 18:06:21 +0200 |
blanchet |
added 'datatype_compat' examples/tests
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 14:54:45 +0000 |
paulson |
New complex analysis material
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
use 'smt2' in SMT examples as much as currently possible
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 11:41:25 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 23:17:55 +0000 |
paulson |
Gauss.thy ported from Old_Number_Theory (unfinished)
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 21:08:03 +0100 |
wenzelm |
more standard theory name;
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 22:08:47 +0100 |
haftmann |
offical tool
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 15:57:02 +0000 |
sultana |
reconstruction framework for LEO-II's TPTP proofs;
|
file |
diff |
annotate
|
| Thu, 13 Feb 2014 12:24:28 +0100 |
wenzelm |
reactivate some examples that still appear to work;
|
file |
diff |
annotate
|
| Thu, 13 Feb 2014 11:54:14 +0100 |
wenzelm |
do not redefine outer syntax commands;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
| Sun, 09 Feb 2014 17:47:23 +0100 |
wenzelm |
minimal document;
|
file |
diff |
annotate
|
| Tue, 04 Feb 2014 21:28:38 +0000 |
paulson |
Restoration of Pocklington.thy. Tidying.
|
file |
diff |
annotate
|
| Sat, 01 Feb 2014 21:43:23 +0100 |
wenzelm |
proper config options;
|
file |
diff |
annotate
|
| Wed, 29 Jan 2014 12:51:37 +0000 |
paulson |
Replacing the theory Library/Binomial by Number_Theory/Binomial
|
file |
diff |
annotate
|
| Thu, 23 Jan 2014 14:26:16 +0100 |
wenzelm |
no document for Cartouche_Examples: avoid problems typesetting "\001";
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
dissolved BNF session
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
minimized Nitpick's dependencies
|
file |
diff |
annotate
|