Mon, 02 Nov 2009 22:24:03 +0100 | krauss | conceal partial rules depending on config flag (i.e. when called via "fun") | changeset | files |
Mon, 02 Nov 2009 22:24:00 +0100 | krauss | conceal "termination" rule, used only by special tools | changeset | files |
Mon, 02 Nov 2009 22:23:57 +0100 | krauss | do not use Binding.empty: conceal flag gets lost in Thm.def_binding_optional | changeset | files |