| Sat, 29 Mar 2008 22:56:01 +0100 |
wenzelm |
functional theory setup -- requires linear access;
|
changeset |
files
|
| Sat, 29 Mar 2008 22:56:00 +0100 |
wenzelm |
simplified print_simpset;
|
changeset |
files
|
| Sat, 29 Mar 2008 22:55:57 +0100 |
wenzelm |
purely functional setup of claset/simpset/clasimpset;
|
changeset |
files
|
| Sat, 29 Mar 2008 22:55:49 +0100 |
wenzelm |
purely functional setup of claset/simpset/clasimpset;
|
changeset |
files
|
| Sat, 29 Mar 2008 19:24:57 +0100 |
wenzelm |
fixed spelling;
|
changeset |
files
|
| Sat, 29 Mar 2008 19:14:16 +0100 |
wenzelm |
added exec_file;
|
changeset |
files
|
| Sat, 29 Mar 2008 19:14:15 +0100 |
wenzelm |
CRITICAL: further trace levels for 1000ms and 100ms;
|
changeset |
files
|
| Sat, 29 Mar 2008 19:14:14 +0100 |
wenzelm |
removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
|
changeset |
files
|
| Sat, 29 Mar 2008 19:14:13 +0100 |
wenzelm |
added generic_theory transaction;
|
changeset |
files
|
| Sat, 29 Mar 2008 19:14:12 +0100 |
wenzelm |
commands 'use' and 'ML' now thy_decl;
|
changeset |
files
|
| Sat, 29 Mar 2008 19:14:11 +0100 |
wenzelm |
removed obsolete use_XXX;
|
changeset |
files
|
| Sat, 29 Mar 2008 19:14:10 +0100 |
wenzelm |
eliminated destructive/critical theorem database;
|
changeset |
files
|
| Sat, 29 Mar 2008 19:14:09 +0100 |
wenzelm |
certify wrt. dynamic context;
|
changeset |
files
|
| Sat, 29 Mar 2008 19:14:08 +0100 |
wenzelm |
added map_theory_result, map_proof_result;
|
changeset |
files
|
| Sat, 29 Mar 2008 19:14:07 +0100 |
wenzelm |
certify wrt. dynamic context;
|
changeset |
files
|