| Fri, 09 May 2014 08:13:36 +0200 | haftmann | removed junk from library theory | changeset | files |
| Fri, 09 May 2014 08:13:28 +0200 | haftmann | note of_class rule for type classes in theory: useful to promote class instance proofs to locale interpretation proofs | changeset | files |
| Fri, 09 May 2014 08:13:26 +0200 | haftmann | normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>; | changeset | files |