| Wed, 07 May 2008 10:56:43 +0200 | berghofe | - Now uses Orderings as parent theory | changeset | files |
| Wed, 07 May 2008 10:56:41 +0200 | berghofe | Deleted instance "set :: (type) power" and moved instance | changeset | files |
| 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 |