Quot/quotient_tacs.ML
Mon, 21 Dec 2009 23:13:40 +0100 Christian Urban used eq_reflection not with OF, but directly in @{thm ...}
less more (0) -1 tip