# HG changeset patch # User wenzelm # Date 1178629289 -7200 # Node ID e2511e6e5cbb5e916359f8923466358f8a56cc24 # Parent e1d3fa78b8e1681446a867865919083bdfb4ae57 updated; diff -r e1d3fa78b8e1 -r e2511e6e5cbb etc/isar-keywords-HOL-Nominal.el --- 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" diff -r e1d3fa78b8e1 -r e2511e6e5cbb etc/isar-keywords-ZF.el --- 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" diff -r e1d3fa78b8e1 -r e2511e6e5cbb etc/isar-keywords.el --- 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"