| Sun, 17 Jun 2007 13:39:39 +0200 | chaieb | thin_prems_tac first max-scopes universal quantifiers; eta_conv moved to Pure/conv.ML | changeset | files |
| Sun, 17 Jun 2007 13:39:34 +0200 | chaieb | Tuned error messages; tuned; | changeset | files |
| Sun, 17 Jun 2007 13:39:32 +0200 | chaieb | normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord) | changeset | files |