| Fri, 09 Sep 1994 11:45:44 +0200 |
lcp |
Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the
|
changeset |
files
|
| Fri, 09 Sep 1994 11:40:40 +0200 |
lcp |
ZF/Zorn/next_bounded: deleted this proof, which was already in comments
|
changeset |
files
|
| Thu, 08 Sep 1994 13:17:57 +0200 |
lcp |
documentation on theories
|
changeset |
files
|
| Thu, 08 Sep 1994 12:55:50 +0200 |
lcp |
ZF/add_ind_def/add_fp_def_i: now prints the fixedpoint defs at the terminal
|
changeset |
files
|
| Thu, 08 Sep 1994 11:05:06 +0200 |
lcp |
{HOL,ZF}/indrule/quant_induct: replaced ssubst in eresolve_tac by
|
changeset |
files
|
| Wed, 07 Sep 1994 17:28:53 +0200 |
lcp |
addition of ZF/ex/twos_compl.thy
|
changeset |
files
|
| Wed, 07 Sep 1994 13:04:28 +0200 |
clasohm |
moved from Contrib
|
changeset |
files
|
| Wed, 07 Sep 1994 10:43:30 +0200 |
clasohm |
renamed temporary variable 'base' to 'thy' in mk_structure
|
changeset |
files
|
| Tue, 06 Sep 1994 14:44:10 +0200 |
clasohm |
renamed base_on into mk_base and moved it to the beginning of the generated
|
changeset |
files
|
| Tue, 06 Sep 1994 13:46:53 +0200 |
lcp |
Pure/type/unvarifyT: moved there from logic.ML
|
changeset |
files
|
| Tue, 06 Sep 1994 13:28:56 +0200 |
lcp |
documentation of theory sections (co)inductive and (co)datatype
|
changeset |
files
|
| Tue, 06 Sep 1994 13:10:38 +0200 |
wenzelm |
minor internal changes;
|
changeset |
files
|