Nominal/nominal_function_core.ML
Thu, 16 Jun 2011 13:14:16 +0100 Christian Urban added eqvt_at and invariant for boths sides of the equations
Tue, 14 Jun 2011 14:07:07 +0100 Christian Urban fixed the problem when giving a complex default-term; the fundef lemmas in Nominal_Base were not general enough
less more (0) -10 -2 tip