| 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 |
| Wed, 10 Jul 2002 16:07:52 +0200 | nipkow | *** empty log message *** | changeset | files |
| Wed, 10 Jul 2002 15:07:02 +0200 | schirmer | Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet). | changeset | files |