src/HOL/Nominal/Nominal.thy
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")