| Wed, 24 Sep 2008 19:33:14 +0200 |
wenzelm |
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
|
changeset |
files
|
| Wed, 24 Sep 2008 19:33:13 +0200 |
wenzelm |
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
|
changeset |
files
|
| Wed, 24 Sep 2008 18:08:42 +0200 |
wenzelm |
init: OuterKeyword.report;
|
changeset |
files
|
| Tue, 23 Sep 2008 23:07:48 +0200 |
wenzelm |
prove_multi: immediate;
|
changeset |
files
|
| Tue, 23 Sep 2008 22:04:30 +0200 |
wenzelm |
added promise_result, prove_promise;
|
changeset |
files
|
| Tue, 23 Sep 2008 18:31:33 +0200 |
berghofe |
Corrected call of SUBPROOF in coherent_tac that used wrong context.
|
changeset |
files
|
| Tue, 23 Sep 2008 18:11:45 +0200 |
haftmann |
fixed outer syntax
|
changeset |
files
|
| Tue, 23 Sep 2008 18:11:44 +0200 |
haftmann |
case default fallback for NBE
|
changeset |
files
|
| Tue, 23 Sep 2008 18:11:43 +0200 |
haftmann |
fixed quickcheck parameter syntax
|
changeset |
files
|
| Tue, 23 Sep 2008 18:11:42 +0200 |
haftmann |
renamed rtype to typerep
|
changeset |
files
|
| Tue, 23 Sep 2008 17:28:58 +0200 |
wenzelm |
added fold_rev;
|
changeset |
files
|
| Tue, 23 Sep 2008 15:48:55 +0200 |
wenzelm |
added del_node, which is more efficient for sparse graphs;
|
changeset |
files
|
| Tue, 23 Sep 2008 15:48:54 +0200 |
wenzelm |
IntGraph.del_node;
|
changeset |
files
|
| Tue, 23 Sep 2008 15:48:53 +0200 |
wenzelm |
join_results: special case for empty list, works without multithreading;
|
changeset |
files
|
| Tue, 23 Sep 2008 15:48:52 +0200 |
wenzelm |
added dest_deriv, removed external type deriv;
|
changeset |
files
|
| Tue, 23 Sep 2008 15:48:51 +0200 |
wenzelm |
added conditional add_oracles, keep oracles_of_proof private;
|
changeset |
files
|
| Tue, 23 Sep 2008 15:48:50 +0200 |
wenzelm |
Thm.proof_of;
|
changeset |
files
|
| Mon, 22 Sep 2008 23:04:35 +0200 |
berghofe |
Added coherent logic prover.
|
changeset |
files
|
| Mon, 22 Sep 2008 23:01:54 +0200 |
berghofe |
New prover for coherent logic.
|
changeset |
files
|
| Mon, 22 Sep 2008 23:00:15 +0200 |
berghofe |
Added setup for coherent logic prover.
|
changeset |
files
|
| Mon, 22 Sep 2008 22:59:35 +0200 |
berghofe |
Added examples for coherent logic prover.
|
changeset |
files
|
| Mon, 22 Sep 2008 22:59:11 +0200 |
berghofe |
Examples for coherent logic prover.
|
changeset |
files
|
| Mon, 22 Sep 2008 19:46:24 +0200 |
urbanc |
made the perm_simp tactic to understand options such as (no_asm)
|
changeset |
files
|
| Mon, 22 Sep 2008 15:26:14 +0200 |
wenzelm |
type thm: fully internal derivation, no longer exported;
|
changeset |
files
|
| Mon, 22 Sep 2008 15:26:14 +0200 |
wenzelm |
added is_finished;
|
changeset |
files
|
| Mon, 22 Sep 2008 15:26:13 +0200 |
wenzelm |
added Promise constructor, which is similar to Oracle but may be replaced later;
|
changeset |
files
|
| Mon, 22 Sep 2008 15:26:11 +0200 |
wenzelm |
removed deriv.ML which is now incorporated into thm.ML;
|
changeset |
files
|
| Mon, 22 Sep 2008 15:26:11 +0200 |
wenzelm |
added reject_draft;
|
changeset |
files
|
| Mon, 22 Sep 2008 15:26:07 +0200 |
wenzelm |
type thm: fully internal derivation, no longer exported;
|
changeset |
files
|
| Mon, 22 Sep 2008 13:56:04 +0200 |
haftmann |
generic quickcheck framework
|
changeset |
files
|