author | narboux |
Thu, 15 Feb 2007 18:18:21 +0100 | |
changeset 22326 | a3acee47a883 |
parent 22325 | be61bd159a99 |
child 22327 | 8a36a3ca8558 |
--- a/src/HOL/Nominal/Nominal.thy Thu Feb 15 17:35:19 2007 +0100 +++ b/src/HOL/Nominal/Nominal.thy Thu Feb 15 18:18:21 2007 +0100 @@ -3008,6 +3008,10 @@ use "nominal_thmdecls.ML" setup "NominalThmDecls.setup" +lemmas [eqvt] = perm_list.simps perm_prod.simps + + + (***************************************) (* setup for the individial atom-kinds *) (* and nominal datatypes *)