Added nominal_primrec command.
authorberghofe
Mon, 27 Nov 2006 12:12:18 +0100
changeset 21544 a9ceeb182cfc
parent 21543 e855f25df0c8
child 21545 54cc492d80a9
Added nominal_primrec command.
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"