| Sun, 09 May 2010 22:06:24 +0200 | wenzelm | reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv; | changeset | files |
| Sun, 09 May 2010 19:50:56 +0200 | wenzelm | Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet; | changeset | files |
| Sun, 09 May 2010 19:15:21 +0200 | wenzelm | just one version of Thm.unconstrainT, which affects all variables; | changeset | files |