Wed, 25 Feb 2009 11:07:10 +0100 | berghofe | Replaced Logic.unvarify by Variable.import_terms to make declaration of | changeset | files |
Wed, 25 Feb 2009 11:05:06 +0100 | berghofe | nominal_inductive and equivariance now work on local_theory. | changeset | files |
Wed, 25 Feb 2009 11:02:25 +0100 | berghofe | Added equivariance lemmas for fresh_star. | changeset | files |