| Fri, 17 Jun 2005 18:33:23 +0200 |
wenzelm |
removed obsolete pretty printers for Theory.theory, Sign.sg;
|
changeset |
files
|
| Fri, 17 Jun 2005 18:33:22 +0200 |
wenzelm |
removed pretty_theory, pprint_theory (see context.ML or thy_info.ML);
|
changeset |
files
|
| Fri, 17 Jun 2005 18:33:21 +0200 |
wenzelm |
added type theory: generic theory contexts with unique identity,
|
changeset |
files
|
| Fri, 17 Jun 2005 18:33:20 +0200 |
wenzelm |
removed Pure/theory_data.ML;
|
changeset |
files
|
| Fri, 17 Jun 2005 18:33:19 +0200 |
wenzelm |
added Id;
|
changeset |
files
|
| Fri, 17 Jun 2005 18:33:18 +0200 |
wenzelm |
Theory.merge;
|
changeset |
files
|
| Fri, 17 Jun 2005 18:33:17 +0200 |
wenzelm |
accomodate change of TheoryDataFun;
|
changeset |
files
|
| Fri, 17 Jun 2005 18:33:16 +0200 |
wenzelm |
Context.theory_name;
|
changeset |
files
|
| Fri, 17 Jun 2005 18:33:15 +0200 |
wenzelm |
accomodate change of TheoryDataFun;
|
changeset |
files
|
| Fri, 17 Jun 2005 18:33:14 +0200 |
wenzelm |
replaced obsolete theory_of_sign by theory_of_thm;
|
changeset |
files
|
| Fri, 17 Jun 2005 18:33:13 +0200 |
wenzelm |
accomodate change of TheoryDataFun;
|
changeset |
files
|
| Fri, 17 Jun 2005 18:33:12 +0200 |
wenzelm |
refer to HOL4_PROOFS setting;
|
changeset |
files
|