Nominal/nominal_function_core.ML
Wed, 22 Jun 2011 12:18:22 +0100 Christian Urban some rudimentary infrastructure for storing data about nominal datatypes
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 -3 tip