| Wed, 07 Feb 2007 18:04:44 +0100 | berghofe | Added functions hhf_proof and un_hhf_proof. | changeset | files |
| Wed, 07 Feb 2007 18:03:18 +0100 | berghofe | Adapted to changes in Accessible_Part and Wellfounded_Recursion theories. | changeset | files |
| Wed, 07 Feb 2007 18:01:40 +0100 | berghofe | Added split_rule attribute. | changeset | files |
| Wed, 07 Feb 2007 18:00:38 +0100 | berghofe | Fixed bug in mk_AbsP. | changeset | files |
| Wed, 07 Feb 2007 17:59:40 +0100 | berghofe | Introduction and elimination rules for <= on predicates | changeset | files |
| Wed, 07 Feb 2007 17:58:50 +0100 | berghofe | - Improved handling of monotonicity rules involving <= | changeset | files |
| Wed, 07 Feb 2007 17:51:38 +0100 | berghofe | Adapted to changes in Finite_Set theory. | changeset | files |
| Wed, 07 Feb 2007 17:46:03 +0100 | berghofe | Adapted to changes in Finite_Set theory. | changeset | files |