| 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
|