| Wed, 07 May 2008 10:56:52 +0200 | berghofe | - Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the | changeset | files |
| Wed, 07 May 2008 10:56:50 +0200 | berghofe | Deleted instantiation "set :: (type) itself". | changeset | files |
| Wed, 07 May 2008 10:56:49 +0200 | berghofe | - Function dec in Trancl_Tac must eta-contract relation before calling | changeset | files |
| 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 |