| Mon, 16 Aug 2010 22:56:28 +0200 |
wenzelm |
HOL-Proofs-Extraction: some workaround to make it work in low-memory situations (e.g. atbroy102 with as little as 1GB heap space);
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 08:59:43 +0200 |
haftmann |
bind and then latex symbols
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 21:12:28 +0200 |
wenzelm |
replaced ML pokes by explicit usedir -p;
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 15:35:14 +0200 |
haftmann |
removed dependency of Euclid on Old_Number_Theory
|
file |
diff |
annotate
|
| Tue, 29 Dec 2009 16:20:39 +0100 |
wenzelm |
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2009 15:39:33 +0200 |
haftmann |
some reorganization of number theory
|
file |
diff |
annotate
|
| Tue, 13 Nov 2007 10:55:54 +0100 |
berghofe |
Added new exampes Greatest_Common_Divisor and Euclid.
|
file |
diff |
annotate
|
| Sat, 10 Nov 2007 14:36:33 +0100 |
wenzelm |
qualified Proofterm.proofs;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 22:21:20 +0200 |
wenzelm |
simultaneous use_thys;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 21:47:39 +0200 |
haftmann |
uniform naming conventions for CG theories
|
file |
diff |
annotate
|
| Fri, 05 Aug 2005 19:57:57 +0200 |
berghofe |
New case study: pigeonhole principle.
|
file |
diff |
annotate
|
| Sun, 21 Jul 2002 15:44:42 +0200 |
berghofe |
Examples for program extraction in HOL.
|
file |
diff |
annotate
|