Thu, 25 Aug 1994 12:09:21 +0200 | lcp | ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without | changeset | files |
Thu, 25 Aug 1994 10:41:17 +0200 | lcp | print_sign_exn: now exported, with a polymorphic type | changeset | files |
Wed, 24 Aug 1994 15:48:47 +0200 | lcp | ZF/ex/LList/lconst_type: streamlined proof | changeset | files |
Tue, 23 Aug 1994 19:34:01 +0200 | wenzelm | added print_syntax: theory -> unit; | changeset | files |
Tue, 23 Aug 1994 19:33:33 +0200 | wenzelm | read_def_cterm: minor changes; | changeset | files |
Tue, 23 Aug 1994 19:31:05 +0200 | wenzelm | removed constant _constrain from Pure sig; | changeset | files |
Mon, 22 Aug 1994 11:27:23 +0200 | lcp | ZF/upair/consE', UnE': new | changeset | files |