| 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 |