# HG changeset patch
# User berghofe
# Date 1164625938 -3600
# Node ID a9ceeb182cfcb7d5513ecf05f92f6b0fd3900011
# Parent  e855f25df0c8e599d099842c6e5905466450b8af
Added nominal_primrec command.

diff -r e855f25df0c8 -r a9ceeb182cfc etc/isar-keywords-HOL-Nominal.el
--- a/etc/isar-keywords-HOL-Nominal.el	Mon Nov 27 12:11:43 2006 +0100
+++ b/etc/isar-keywords-HOL-Nominal.el	Mon Nov 27 12:12:18 2006 +0100
@@ -116,6 +116,7 @@
     "no_syntax"
     "no_translations"
     "nominal_datatype"
+    "nominal_primrec"
     "nonterminals"
     "normal_form"
     "notation"
@@ -240,6 +241,7 @@
     "file"
     "fixes"
     "for"
+    "freshness_context"
     "hints"
     "if"
     "imports"
@@ -251,6 +253,7 @@
     "infixr"
     "inject"
     "intros"
+    "invariant"
     "is"
     "monos"
     "morphisms"
@@ -453,6 +456,7 @@
     "instance"
     "interpretation"
     "lemma"
+    "nominal_primrec"
     "recdef_tc"
     "specification"
     "termination"