| Wed, 07 May 2008 10:56:40 +0200 | berghofe | split_beta is now declared as monotonicity rule, to allow bounded | changeset | files |
| Wed, 07 May 2008 10:56:39 +0200 | berghofe | - Added mem_def and predicate1I in some of the proofs | changeset | files |
| Wed, 07 May 2008 10:56:38 +0200 | berghofe | - Now imports Code_Setup, rather than Set and Fun, since the theorems | changeset | files |
| Wed, 07 May 2008 10:56:37 +0200 | berghofe | - Explicitely applied predicate1I in a few proofs, because it is no longer | changeset | files |