--- a/etc/isar-keywords.el Thu May 22 15:31:36 2014 +0200
+++ b/etc/isar-keywords.el Thu May 22 15:49:36 2014 +0200
@@ -149,9 +149,11 @@
"no_translations"
"no_type_notation"
"nominal_datatype"
+ "nominal_function"
"nominal_inductive"
"nominal_inductive2"
"nominal_primrec"
+ "nominal_termination"
"nonterminal"
"notation"
"note"
@@ -315,6 +317,7 @@
"avoids"
"begin"
"binder"
+ "binds"
"checking"
"class_instance"
"class_relation"
@@ -613,9 +616,11 @@
"interpretation"
"lemma"
"lift_definition"
+ "nominal_function"
"nominal_inductive"
"nominal_inductive2"
"nominal_primrec"
+ "nominal_termination"
"pcpodef"
"permanent_interpretation"
"primcorecursive"
--- a/src/HOL/ROOT Thu May 22 15:31:36 2014 +0200
+++ b/src/HOL/ROOT Thu May 22 15:49:36 2014 +0200
@@ -582,6 +582,7 @@
ML
SAT_Examples
Sudoku
+ Nominal2_Dummy
theories [skip_proofs = false]
Meson_Test
theories [condition = SVC_HOME]
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Nominal2_Dummy.thy Thu May 22 15:49:36 2014 +0200
@@ -0,0 +1,22 @@
+header \<open>Dummy theory to anticipate AFP/Nominal2 keywords\<close> (* Proof General legacy *)
+
+theory Nominal2_Dummy
+imports Main
+keywords
+ "nominal_datatype" :: thy_decl and
+ "nominal_function" "nominal_inductive" "nominal_termination" :: thy_goal and
+ "atom_decl" "equivariance" :: thy_decl and
+ "avoids" "binds"
+begin
+
+ML \<open>
+Outer_Syntax.command @{command_spec "nominal_datatype"} "dummy" Scan.fail;
+Outer_Syntax.command @{command_spec "nominal_function"} "dummy" Scan.fail;
+Outer_Syntax.command @{command_spec "nominal_inductive"} "dummy" Scan.fail;
+Outer_Syntax.command @{command_spec "nominal_termination"} "dummy" Scan.fail;
+Outer_Syntax.command @{command_spec "atom_decl"} "dummy" Scan.fail;
+Outer_Syntax.command @{command_spec "equivariance"} "dummy" Scan.fail;
+\<close>
+
+end
+