| Fri, 13 Mar 2009 19:17:58 +0100 |
haftmann |
coherent binding policy with primitive target operations
|
changeset |
files
|
| Fri, 13 Mar 2009 19:17:57 +0100 |
haftmann |
moved some generic nonsense to arith_data.ML
|
changeset |
files
|
| Fri, 13 Mar 2009 19:17:57 +0100 |
haftmann |
tuned ML code
|
changeset |
files
|
| Fri, 13 Mar 2009 10:14:47 -0700 |
huffman |
remove legacy ML bindings
|
changeset |
files
|
| Fri, 13 Mar 2009 23:50:05 +0100 |
wenzelm |
simplified method setup;
|
changeset |
files
|
| Fri, 13 Mar 2009 23:32:40 +0100 |
wenzelm |
simplified goal_spec: default to first goal;
|
changeset |
files
|
| Fri, 13 Mar 2009 21:25:15 +0100 |
wenzelm |
eliminated type Args.T;
|
changeset |
files
|
| Fri, 13 Mar 2009 21:24:21 +0100 |
wenzelm |
added simplified setup;
|
changeset |
files
|
| Fri, 13 Mar 2009 21:22:45 +0100 |
wenzelm |
pervasive types 'a parser and 'a context_parser;
|
changeset |
files
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
changeset |
files
|
| Fri, 13 Mar 2009 19:53:09 +0100 |
wenzelm |
more regular method setup via SIMPLE_METHOD;
|
changeset |
files
|
| Fri, 13 Mar 2009 19:10:46 +0100 |
wenzelm |
tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
|
changeset |
files
|
| Fri, 13 Mar 2009 15:52:23 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 13 Mar 2009 07:35:18 -0700 |
huffman |
fix typed print translation for CARD('a)
|
changeset |
files
|
| Fri, 13 Mar 2009 07:30:47 -0700 |
huffman |
introduce new helper functions; clean up proofs
|
changeset |
files
|