| Thu, 11 Jul 2002 09:47:15 +0200 | nipkow | Added partly automated version of Newman. | changeset | files |
| Thu, 11 Jul 2002 09:36:41 +0200 | schirmer | Fixed markup error in comment. | changeset | files |
| Thu, 11 Jul 2002 09:31:01 +0200 | nipkow | *** empty log message *** | changeset | files |
| Thu, 11 Jul 2002 09:17:01 +0200 | nipkow | *** empty log message *** | changeset | files |
| Wed, 10 Jul 2002 18:39:15 +0200 | berghofe | expand_proof now also takes an optional term describing the proposition | changeset | files |
| Wed, 10 Jul 2002 18:37:51 +0200 | berghofe | - Moved abs_def to drule.ML | changeset | files |
| Wed, 10 Jul 2002 18:35:34 +0200 | berghofe | Simplified proof of induction rule for datatypes involving function types. | changeset | files |
| Wed, 10 Jul 2002 16:54:07 +0200 | paulson | Fixed quantified variable name preservation for ball and bex (bounded quants) | changeset | files |