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