Sun, 09 May 2010 09:39:01 -0700 | huffman | merged | changeset | files |
Sat, 08 May 2010 17:06:58 -0700 | huffman | add lemmas one_less_inverse and one_le_inverse | changeset | files |
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 |