changeset 46950 | d0181abdbdac |
parent 46947 | b8c7eb0c2f89 |
child 47108 | 2a1953f0d20d |
--- a/src/HOL/Nominal/Nominal.thy Thu Mar 15 20:07:00 2012 +0100 +++ b/src/HOL/Nominal/Nominal.thy Thu Mar 15 22:08:53 2012 +0100 @@ -1,6 +1,9 @@ theory Nominal imports Main "~~/src/HOL/Library/Infinite_Set" -keywords "avoids" +keywords + "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and + "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and + "avoids" uses ("nominal_thmdecls.ML") ("nominal_atoms.ML")