--- a/etc/isar-keywords-HOL-Nominal.el Tue May 08 15:01:28 2007 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el Tue May 08 15:01:29 2007 +0200
@@ -11,7 +11,6 @@
"ML"
"ML_command"
"ML_setup"
- "ProofGeneral\\.call_atp"
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
"ProofGeneral\\.kill_proof"
@@ -184,6 +183,7 @@
"setup"
"show"
"simproc_setup"
+ "sledgehammer"
"sorry"
"specification"
"subsect"
@@ -299,7 +299,6 @@
(defconst isar-keywords-diag
'("ML"
"ML_command"
- "ProofGeneral\\.call_atp"
"cd"
"class_deps"
"code_deps"
@@ -347,6 +346,7 @@
"quickcheck"
"refute"
"remove_thy"
+ "sledgehammer"
"term"
"thm"
"thm_deps"
--- a/etc/isar-keywords-ZF.el Tue May 08 15:01:28 2007 +0200
+++ b/etc/isar-keywords-ZF.el Tue May 08 15:01:29 2007 +0200
@@ -42,6 +42,7 @@
"code_class"
"code_const"
"code_datatype"
+ "code_deps"
"code_gen"
"code_instance"
"code_library"
@@ -277,6 +278,7 @@
"ML_command"
"cd"
"class_deps"
+ "code_deps"
"code_gen"
"code_thms"
"commit"
--- a/etc/isar-keywords.el Tue May 08 15:01:28 2007 +0200
+++ b/etc/isar-keywords.el Tue May 08 15:01:29 2007 +0200
@@ -11,7 +11,6 @@
"ML"
"ML_command"
"ML_setup"
- "ProofGeneral\\.call_atp"
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
"ProofGeneral\\.kill_proof"
@@ -44,6 +43,7 @@
"code_class"
"code_const"
"code_datatype"
+ "code_deps"
"code_gen"
"code_instance"
"code_library"
@@ -184,6 +184,7 @@
"setup"
"show"
"simproc_setup"
+ "sledgehammer"
"sorry"
"specification"
"subsect"
@@ -313,9 +314,9 @@
(defconst isar-keywords-diag
'("ML"
"ML_command"
- "ProofGeneral\\.call_atp"
"cd"
"class_deps"
+ "code_deps"
"code_gen"
"code_thms"
"commit"
@@ -360,6 +361,7 @@
"quickcheck"
"refute"
"remove_thy"
+ "sledgehammer"
"term"
"thm"
"thm_deps"