| Thu, 18 Sep 2008 19:39:49 +0200 | wenzelm | begin_theory: Theory.checkpoint for immediate uses ensures that ML evaluation always starts with non-draft @{theory}; | changeset | files |
| Thu, 18 Sep 2008 19:39:47 +0200 | wenzelm | updated generated file; | changeset | files |
| Thu, 18 Sep 2008 19:39:44 +0200 | wenzelm | simplified oracle interface; | changeset | files |
| Thu, 18 Sep 2008 14:06:58 +0200 | wenzelm | show: non-critical testing; | changeset | files |
| Thu, 18 Sep 2008 14:06:56 +0200 | wenzelm | added deriv.ML: Abstract derivations based on raw proof terms. | changeset | files |
| Thu, 18 Sep 2008 12:13:50 +0200 | krauss | termination prover for "fun" can be configured using context data. | changeset | files |