| Thu, 03 Jun 2010 16:39:50 +0200 | krauss | clarified | changeset | files |
| Thu, 03 Jun 2010 16:39:05 +0200 | krauss | mention unconstrain in NEWS | changeset | files |
| Wed, 02 Jun 2010 22:45:50 +0200 | haftmann | merged | changeset | files |
| Wed, 02 Jun 2010 22:06:14 +0200 | haftmann | hide default, map_entry, map_default | changeset | files |
| Wed, 02 Jun 2010 21:53:03 +0200 | wenzelm | improved parallelism of proof term normalization; | changeset | files |
| Wed, 02 Jun 2010 21:39:35 +0200 | wenzelm | always unconstrain thm proofs; | changeset | files |
| Wed, 02 Jun 2010 21:12:28 +0200 | wenzelm | replaced ML pokes by explicit usedir -p; | changeset | files |
| Wed, 02 Jun 2010 18:48:30 +0200 | haftmann | merged | changeset | files |
| Wed, 02 Jun 2010 16:24:14 +0200 | haftmann | absolute import -- must work with Main.thy / HOL-Proofs | changeset | files |
| Wed, 02 Jun 2010 16:24:14 +0200 | haftmann | avoid duplicate import | changeset | files |
| Wed, 02 Jun 2010 16:24:14 +0200 | haftmann | HOL-Proofs is based in Main.thy | changeset | files |
| Wed, 02 Jun 2010 16:24:13 +0200 | haftmann | dropped lemma duplicate | changeset | files |
| Wed, 02 Jun 2010 15:35:14 +0200 | haftmann | msetprod_empty, msetprod_singleton | changeset | files |
| Wed, 02 Jun 2010 15:35:14 +0200 | haftmann | induction over non-empty lists | changeset | files |
| Wed, 02 Jun 2010 15:35:14 +0200 | haftmann | removed dependency of Euclid on Old_Number_Theory | changeset | files |
| Wed, 02 Jun 2010 15:35:13 +0200 | haftmann | modernized | changeset | files |
| Wed, 02 Jun 2010 16:42:58 +0200 | wenzelm | removed obsolete usedir -p 1 option; | changeset | files |
| Wed, 02 Jun 2010 15:38:27 +0200 | wenzelm | actually test smlnj; | changeset | files |
| Wed, 02 Jun 2010 15:36:24 +0200 | wenzelm | updated keywords; | changeset | files |
| Wed, 02 Jun 2010 14:55:37 +0200 | wenzelm | Added tag isa2009-2-test0 for changeset 935c75359742 | changeset | files |
| Wed, 02 Jun 2010 14:38:39 +0200 | wenzelm | more CONTRIBUTORS; | changeset | files |
| Wed, 02 Jun 2010 13:18:48 +0200 | wenzelm | merged | changeset | files |
| Wed, 02 Jun 2010 13:18:21 +0200 | wenzelm | Hilbert_Classical: disable multithreading altogether, otherwise proof normalization will fork futures independently of Goal.parallel_proofs; | changeset | files |
| Wed, 02 Jun 2010 12:40:25 +0200 | nipkow | merged | changeset | files |
| Wed, 02 Jun 2010 12:40:12 +0200 | nipkow | added lemmas | changeset | files |
| Wed, 02 Jun 2010 11:53:17 +0200 | blanchet | merged | changeset | files |
| Wed, 02 Jun 2010 10:51:55 +0200 | blanchet | merge | changeset | files |
| Wed, 02 Jun 2010 10:50:53 +0200 | blanchet | fix parameter settings | changeset | files |