--- a/ProgTutorial/Helper/isar-keywords-command.el	Fri Aug 21 16:23:51 2009 +0200
+++ b/ProgTutorial/Helper/isar-keywords-command.el	Sat Aug 22 02:56:08 2009 +0200
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + HOL + Pure-ProofGeneral + HOL-Command.
+;; Generated from Pure + Pure-ProofGeneral + HOL + HOL-Command.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
@@ -97,6 +97,9 @@
     "find_theorems"
     "fix"
     "foobar"
+    "foobar_goal"
+    "foobar_prove"
+    "foobar_trace"
     "from"
     "full_prf"
     "fun"
@@ -197,7 +200,7 @@
     "section"
     "setup"
     "show"
-    "simple_induct"
+    "simple_inductive"
     "simproc_setup"
     "sledgehammer"
     "sorry"
@@ -433,6 +436,8 @@
     "extract"
     "extract_type"
     "finalconsts"
+    "foobar"
+    "foobar_trace"
     "fun"
     "global"
     "hide"
@@ -464,7 +469,7 @@
     "record"
     "refute_params"
     "setup"
-    "simple_induct"
+    "simple_inductive"
     "simproc_setup"
     "syntax"
     "text"
@@ -484,7 +489,8 @@
   '("ax_specification"
     "code_pred"
     "corollary"
-    "foobar"
+    "foobar_goal"
+    "foobar_prove"
     "function"
     "instance"
     "interpretation"