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