Sun, 09 May 2010 15:28:44 +0200 | krauss | do not redeclare [simp] rules, to avoid "duplicate rewrite rule" warnings | changeset | files |
Sun, 09 May 2010 12:00:43 +0200 | krauss | added lemmas rel_comp_UNION_distrib(2) | changeset | files |
Sat, 08 May 2010 22:29:44 +0200 | wenzelm | made SML/NJ happy; | changeset | files |
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 |