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