| 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
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
moved BNF examples
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
killed obsolete session
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:55 +0100 |
blanchet |
moved subset of 'HOL-Cardinals' needed for BNF into 'HOL'
|
file |
diff |
annotate
|
| Sat, 18 Jan 2014 19:15:12 +0100 |
wenzelm |
support for nested text cartouches;
|
file |
diff |
annotate
|
| Thu, 16 Jan 2014 16:33:19 +0100 |
blanchet |
moved 'Zorn' into 'Main', since it's a BNF dependency
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 11:47:10 +0100 |
traytel |
new codatatype example: stream processors
|
file |
diff |
annotate
|
| Mon, 18 Nov 2013 18:04:45 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
| Mon, 18 Nov 2013 18:04:44 +0100 |
blanchet |
split 'Cardinal_Arithmetic' 3-way
|
file |
diff |
annotate
|
| Mon, 18 Nov 2013 18:04:44 +0100 |
blanchet |
started three-way split of 'HOL-Cardinals'
|
file |
diff |
annotate
|
| Sat, 16 Nov 2013 18:34:11 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sat, 16 Nov 2013 16:57:09 +0100 |
wenzelm |
proper thy_load command 'boogie_file' -- avoid direct access to file-system;
|
file |
diff |
annotate
|
| Thu, 14 Nov 2013 13:03:09 +0100 |
haftmann |
explicit inclusion of data refinement theory into HOL-Library session
|
file |
diff |
annotate
|
| Wed, 23 Oct 2013 14:53:36 +0200 |
blanchet |
added 'primcorec' examples
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 22:34:43 +0200 |
wenzelm |
added Isabelle/ML example;
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 00:01:10 +0200 |
blanchet |
register codatatypes with Nitpick
|
file |
diff |
annotate
|
| Tue, 17 Sep 2013 14:10:33 +0200 |
kuncar |
include Int_Pow into Quotient_Examples; add end of the theory
|
file |
diff |
annotate
|
| Fri, 06 Sep 2013 10:56:40 +0200 |
noschinl |
added examples for Simps_Case_Conv
|
file |
diff |
annotate
|
| Fri, 30 Aug 2013 12:06:11 +0200 |
blanchet |
added example
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 12:40:55 +0200 |
wenzelm |
clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL;
|
file |
diff |
annotate
|
| Wed, 21 Aug 2013 09:25:40 +0200 |
blanchet |
renamed theory files to be closer to (new) command names
|
file |
diff |
annotate
|
| Wed, 24 Jul 2013 22:54:47 +0200 |
nipkow |
merged Def_Init_Sound_X into Def_Init_X
|
file |
diff |
annotate
|
| Tue, 23 Jul 2013 18:36:23 +0200 |
boehmes |
removed obsolete HOL-Boogie session;
|
file |
diff |
annotate
|
| Tue, 02 Jul 2013 14:48:01 +0200 |
wenzelm |
clarified Proofterm.proofs vs. Goal.skip_proofs;
|
file |
diff |
annotate
|
| Sun, 30 Jun 2013 12:30:02 +0200 |
wenzelm |
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 16:47:45 +0200 |
wenzelm |
support for XML data representation of proof terms;
|
file |
diff |
annotate
|
| Thu, 20 Jun 2013 17:26:16 +0200 |
nipkow |
tuned theory name
|
file |
diff |
annotate
|
| Wed, 19 Jun 2013 10:14:50 +0200 |
nipkow |
more canonical name (2)
|
file |
diff |
annotate
|
| Mon, 10 Jun 2013 20:30:23 +0200 |
haftmann |
dropped relics of ancient binary numeral case study
|
file |
diff |
annotate
|
| Sat, 01 Jun 2013 12:02:41 +0200 |
nipkow |
tuned theory name
|
file |
diff |
annotate
|
| Fri, 31 May 2013 11:56:48 +0200 |
wenzelm |
make SML/NJ partially happy;
|
file |
diff |
annotate
|
| Fri, 31 May 2013 07:55:09 +0200 |
nipkow |
more VC -> VCG
|
file |
diff |
annotate
|
| Thu, 30 May 2013 20:09:49 +0200 |
bulwahn |
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
|
file |
diff |
annotate
|
| Wed, 29 May 2013 23:11:21 +0200 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| 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
|