# HG changeset patch
# User berghofe
# Date 1175011062 -7200
# Node ID 7b9f346ac3662cc09e49ff502486b6159e6571d8
# Parent  1cbfb4066e47c3446bb421dd29614e6698bcbe97
Adapted to new syntax of nominal_inductive.

diff -r 1cbfb4066e47 -r 7b9f346ac366 etc/isar-keywords-HOL-Nominal.el
--- a/etc/isar-keywords-HOL-Nominal.el	Tue Mar 27 17:57:05 2007 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el	Tue Mar 27 17:57:42 2007 +0200
@@ -44,6 +44,7 @@
     "code_class"
     "code_const"
     "code_datatype"
+    "code_deps"
     "code_gen"
     "code_instance"
     "code_library"
@@ -76,6 +77,7 @@
     "done"
     "enable_pr"
     "end"
+    "equivariance"
     "exit"
     "extract"
     "extract_type"
@@ -235,6 +237,7 @@
     "and"
     "assumes"
     "attach"
+    "avoids"
     "begin"
     "binder"
     "concl"
@@ -299,6 +302,7 @@
     "ProofGeneral\\.call_atp"
     "cd"
     "class_deps"
+    "code_deps"
     "code_gen"
     "code_thms"
     "commit"
@@ -410,6 +414,7 @@
     "defer_recdef"
     "definition"
     "defs"
+    "equivariance"
     "extract"
     "extract_type"
     "finalconsts"
@@ -426,7 +431,6 @@
     "no_syntax"
     "no_translations"
     "nominal_datatype"
-    "nominal_inductive"
     "nonterminals"
     "notation"
     "oracle"
@@ -467,6 +471,7 @@
     "instance"
     "interpretation"
     "lemma"
+    "nominal_inductive"
     "nominal_primrec"
     "recdef_tc"
     "specification"