Wed, 22 Mar 2006 12:33:44 +0100 | paulson | Introduction of "whitelist": theorems forced past the relevance filter | changeset | files |
Wed, 22 Mar 2006 12:32:44 +0100 | paulson | Slight simplification of proofs | changeset | files |
Wed, 22 Mar 2006 12:30:29 +0100 | paulson | Removal of obsolete strategies. Initial support for locales: Frees and Consts | changeset | files |
Wed, 22 Mar 2006 11:54:54 +0100 | webertj | comment for conjI added | changeset | files |
Wed, 22 Mar 2006 11:14:58 +0100 | nipkow | translations -> abbreviations (a cool feature) | changeset | files |
Tue, 21 Mar 2006 15:38:53 +0100 | wenzelm | fixed example; | changeset | files |
Tue, 21 Mar 2006 12:18:22 +0100 | wenzelm | mark_boundT: produce well-typed term; | changeset | files |