Quot/quotient_tacs.ML
Tue, 22 Dec 2009 07:28:09 +0100 Christian Urban simplified calculate_instance; worked around some clever code; clever code is unfortunately still there...needs to be removed
Mon, 21 Dec 2009 23:13:40 +0100 Christian Urban used eq_reflection not with OF, but directly in @{thm ...}
less more (0) -2 tip