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