| Fri, 05 Apr 2013 18:31:35 +0200 |
nipkow |
tuned document
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 21:07:10 +0100 |
wenzelm |
separate isatest with skip_proofs, to give some impression of performance without most of the proofs;
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 19:32:44 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 18:04:21 +0100 |
wenzelm |
allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 16:38:25 +0100 |
wenzelm |
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 20:37:32 +0100 |
wenzelm |
tuned session specification;
|
file |
diff |
annotate
|
| Mon, 25 Mar 2013 20:00:27 +0100 |
ballarin |
Discontinued theories src/HOL/Algebra/abstract and .../poly.
|
file |
diff |
annotate
|
| Wed, 13 Mar 2013 17:15:25 +0100 |
wenzelm |
proper formatting, to facilitate line-based diff;
|
file |
diff |
annotate
|
| Wed, 13 Mar 2013 17:13:22 +0100 |
wenzelm |
more uniform session descriptions, which show up in chapter index;
|
file |
diff |
annotate
|
| Tue, 12 Mar 2013 21:59:48 +0100 |
wenzelm |
refurbished some old README.html files as session descriptions, which show up in chapter index;
|
file |
diff |
annotate
|
| Mon, 11 Mar 2013 13:28:46 +0100 |
wenzelm |
support for 'chapter' specifications within session ROOT;
|
file |
diff |
annotate
|
| Sun, 24 Feb 2013 20:29:13 +0100 |
haftmann |
turned example into library for comparing growth of functions
|
file |
diff |
annotate
|
| Thu, 21 Feb 2013 18:21:40 +0100 |
wenzelm |
more explicit session dependency, for improved parallel performance of HOL-UNITY test session -- NB: separate 'theories' sections are sequential;
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 11:47:34 +0100 |
haftmann |
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 11:47:33 +0100 |
haftmann |
systematic conversions between nat and nibble/char;
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 14:14:55 +0100 |
haftmann |
consolidation of library theories on product orders
|
file |
diff |
annotate
|
| Wed, 13 Feb 2013 13:38:52 +0100 |
haftmann |
tuned, particulary name
|
file |
diff |
annotate
|
| Sat, 19 Jan 2013 22:18:35 +0100 |
wenzelm |
afford parallel proof terms;
|
file |
diff |
annotate
|
| Sun, 13 Jan 2013 22:05:47 +0100 |
wenzelm |
hardwired document_variants, to prevent HOL-IMP's \snip choking on macros from isabellestags.sty;
|
file |
diff |
annotate
|
| Sat, 12 Jan 2013 14:56:57 +0100 |
wenzelm |
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 14:33:44 +0100 |
wenzelm |
discontinued HOL side-entry sessions -- may be configured in $ISABELLE_HOME_USER/ROOT instead;
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 09:31:25 +0100 |
blanchet |
actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 09:13:50 +0100 |
blanchet |
added missing certificate file to "ROOT"
|
file |
diff |
annotate
|
| Sat, 29 Dec 2012 17:18:01 +0100 |
nipkow |
new theory Library/Finite_Lattice
|
file |
diff |
annotate
|
| Sun, 16 Dec 2012 21:27:23 +0100 |
wenzelm |
HOL-Quickcheck_Benchmark works without timeout (NB: isatest imposes global timeout already);
|
file |
diff |
annotate
|
| Sun, 16 Dec 2012 18:12:18 +0100 |
bulwahn |
reverting d466ebc27810 as the previous changeset should allow to run Find_Unused_Assms_Examples again
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 15:36:08 +0100 |
traytel |
renamed theory
|
file |
diff |
annotate
|
| Tue, 11 Dec 2012 22:19:39 +0100 |
wenzelm |
disable Find_Unused_Assms_Examples for now, to recover isatest sanity;
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 18:00:40 +0100 |
hoelzl |
remove SMT proofs in Multivariate_Analysis
|
file |
diff |
annotate
|
| Fri, 23 Nov 2012 22:16:52 +0100 |
wenzelm |
timeout in proper place (HOL-Quickcheck_Examples approx. 1min, HOL-Quickcheck_Benchmark approx. 1h);
|
file |
diff |
annotate
|
| Thu, 22 Nov 2012 08:23:13 +0100 |
nipkow |
tuned names
|
file |
diff |
annotate
|
| Wed, 21 Nov 2012 15:50:54 +0100 |
wenzelm |
more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2012 09:07:41 +0100 |
nipkow |
new theory of immutable arrays
|
file |
diff |
annotate
|
| Mon, 12 Nov 2012 12:27:58 +0100 |
nipkow |
new theory IMP/Finite_Reachable
|
file |
diff |
annotate
|
| Thu, 08 Nov 2012 10:02:38 +0100 |
haftmann |
refined stack of library theories implementing int and/or nat by target language numerals
|
file |
diff |
annotate
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
moved Refute to "HOL/Library" to speed up building "Main" even more
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 20:00:45 +0200 |
wenzelm |
back to parallel HOL-BNF-Examples, which seems to have suffered from Future.map on canceled persistent futures;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2012 22:57:28 +0200 |
wenzelm |
HOL-BNF-Examples is sequential for now, due to spurious interrupts (again);
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 13:15:58 +0200 |
popescua |
update ROOT with teh directory change in BNF
|
file |
diff |
annotate
|
| Wed, 03 Oct 2012 22:07:26 +0200 |
blanchet |
thread the right local theory through + reenable parallel proofs for previously problematic theories
|
file |
diff |
annotate
|
| Thu, 27 Sep 2012 00:40:51 +0200 |
blanchet |
modernized examples;
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:41:36 +0200 |
blanchet |
disable parallel proofs for two big examples -- speeds up things and eliminates spurious Interrupt exceptions (to be investigated)
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 18:25:17 +0200 |
blanchet |
changed base session for "HOL-BNF" for faster building in the typical case
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 16:53:38 +0200 |
blanchet |
created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 16:45:06 +0200 |
blanchet |
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
|
file |
diff |
annotate
|
| Thu, 20 Sep 2012 17:25:07 +0200 |
blanchet |
the Codatatype package currently needs all of Cardinals (temporary -- because of countable sets)
|
file |
diff |
annotate
|
| Wed, 19 Sep 2012 21:06:35 +0200 |
wenzelm |
reactivate HOL-Mirabelle-ex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 13:38:10 +0200 |
popescua |
added top-level theory for Cardinals
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 15:38:16 +0200 |
wenzelm |
bypass HOL-Mirabelle-ex in regular test, until its tendency to "hang" has been resolved;
|
file |
diff |
annotate
|
| Thu, 13 Sep 2012 16:43:33 +0200 |
wenzelm |
workaround for HOL-Mirabelle-ex oddities;
|
file |
diff |
annotate
|
| Wed, 12 Sep 2012 05:29:21 +0200 |
blanchet |
renamed "Ordinals_and_Cardinals" to "Cardinals"
|
file |
diff |
annotate
|
| Tue, 04 Sep 2012 12:12:03 +0200 |
traytel |
eliminated obsolete "parallel_proofs = 0" restriction (cf. 0e5b859e1c91)
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 10:27:56 +0900 |
Christian Sternagel |
renamed theory List_Prefix into Sublist (since it is not only about prefixes)
|
file |
diff |
annotate
|
| Tue, 28 Aug 2012 18:46:15 +0200 |
wenzelm |
do not hardwire document output options -- to be provided by the user;
|
file |
diff |
annotate
|
| Tue, 28 Aug 2012 17:17:41 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 28 Aug 2012 17:17:03 +0200 |
blanchet |
documentation cleanup
|
file |
diff |
annotate
|
| Tue, 28 Aug 2012 17:16:00 +0200 |
blanchet |
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
|
file |
diff |
annotate
|
| Sun, 19 Aug 2012 17:45:07 +0200 |
wenzelm |
actual use of (sos remote_csdp) via ISABELLE_FULL_TEST;
|
file |
diff |
annotate
|
| Thu, 23 Aug 2012 12:55:23 +0200 |
wenzelm |
more basic file dependencies -- no load command here;
|
file |
diff |
annotate
|
| Sat, 11 Aug 2012 11:31:05 +0200 |
nipkow |
special code with lists no longer necessary, use sets
|
file |
diff |
annotate
|
| Wed, 08 Aug 2012 17:49:56 +0200 |
wenzelm |
simplified session specifications: names are taken verbatim and current directory is default;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 23:38:18 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 06 Aug 2012 11:59:09 +0200 |
wenzelm |
more precise imitation of old ROOT.ML files;
|
file |
diff |
annotate
|
| Sat, 04 Aug 2012 22:50:56 +0200 |
wenzelm |
some timeouts, which modify the build order;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2012 15:56:36 +0200 |
wenzelm |
added offline test for skip_proofs;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2012 15:50:50 +0200 |
wenzelm |
clarified ISABELLE_FULL_TEST;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2012 19:55:04 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 31 Jul 2012 14:43:55 +0200 |
kuncar |
Remove Lift_RBT.thy, it's in HOL/Library/RBT.thy now
|
file |
diff |
annotate
|
| Tue, 31 Jul 2012 13:55:39 +0200 |
kuncar |
add testing file for RBT_Set
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 15:55:19 +0200 |
bulwahn |
moved another larger quickcheck example to Quickcheck_Benchmark
|
file |
diff |
annotate
|
| Tue, 31 Jul 2012 16:26:12 +0200 |
wenzelm |
HOL-Probability appears to work with smlnj;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2012 12:38:01 +0200 |
wenzelm |
renamed session TLA to HOL-TLA to avoid clash with AFP;
|
file |
diff |
annotate
|
| Mon, 30 Jul 2012 12:08:25 +0200 |
wenzelm |
updated ROOT according to 3defa60a7ae3;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2012 20:36:25 +0200 |
wenzelm |
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2012 20:27:39 +0200 |
wenzelm |
added Quickcheck_Benchmark (cf. 1959baa22632);
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 13:35:31 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 12:27:47 +0200 |
wenzelm |
support session groups;
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 11:52:08 +0200 |
wenzelm |
discontinued slightly odd session order, which did not quite work out;
|
file |
diff |
annotate
|
| Wed, 25 Jul 2012 11:59:22 +0200 |
wenzelm |
added condition = ISABELLE_POLYML according to no-smlnj targets in IsaMakefile;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2012 22:00:12 +0200 |
wenzelm |
more files;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2012 21:54:49 +0200 |
wenzelm |
more build options;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2012 21:36:53 +0200 |
wenzelm |
tuned order;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2012 21:26:28 +0200 |
wenzelm |
more build options;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2012 20:42:34 +0200 |
wenzelm |
more explicit document = false to reduce warnings;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2012 18:38:07 +0200 |
wenzelm |
more session entries;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2012 12:38:33 +0200 |
wenzelm |
clarified "document" again, eliminated redundant "no_document";
|
file |
diff |
annotate
|
| Tue, 24 Jul 2012 10:11:49 +0200 |
wenzelm |
clarified document options;
|
file |
diff |
annotate
|
| Sat, 21 Jul 2012 22:13:50 +0200 |
wenzelm |
propagate defined options;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2012 14:24:40 +0200 |
wenzelm |
support Session.Queue with ordering and dependencies;
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 17:22:59 +0200 |
wenzelm |
some HOL sessions;
|
file |
diff |
annotate
|