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 ...}
Mon, 21 Dec 2009 23:01:58 +0100 Christian Urban cleaned a bit calculate_inst a bit; eta-contraction seems to be not necessary? (all examples go through)
less more (0) -3 tip