Added new "value" command.

--- a/etc/isar-keywords-ZF.el	Wed Sep 21 12:02:56 2005 +0200
+++ b/etc/isar-keywords-ZF.el	Wed Sep 21 12:03:41 2005 +0200
@@ -156,7 +156,6 @@
     "theory"
     "thm"
     "thm_deps"
-    "thms_containing"
     "thus"
     "token_translation"
     "touch_all_thys"
@@ -179,6 +178,7 @@
     "use_thy"
     "use_thy_only"
     "using"
+    "value"
     "welcome"
     "with"
     "{"
@@ -287,7 +287,6 @@
     "term"
     "thm"
     "thm_deps"
-    "thms_containing"
     "touch_all_thys"
     "touch_child_thys"
     "touch_thy"
@@ -297,6 +296,7 @@
     "use"
     "use_thy"
     "use_thy_only"
+    "value"
     "welcome"))
 
 (defconst isar-keywords-theory-begin

--- a/etc/isar-keywords.el	Wed Sep 21 12:02:56 2005 +0200
+++ b/etc/isar-keywords.el	Wed Sep 21 12:03:41 2005 +0200
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; This file was generated by Isabelle/HOLCF/IOA/Complex/Import -- DO NOT EDIT!
+;; This file was generated by Isabelle/HOLCF/IOA -- DO NOT EDIT!
 ;;
 ;; $Id$
 ;;
@@ -22,7 +22,6 @@
     "ProofGeneral\\.try_context_thy_only"
     "ProofGeneral\\.undo"
     "also"
-    "append_dump"
     "apply"
     "apply_end"
     "arities"
@@ -44,9 +43,6 @@
     "code_module"
     "coinductive"
     "commit"
-    "const_maps"
-    "const_moves"
-    "const_renames"
     "constdefs"
     "consts"
     "consts_code"
@@ -56,7 +52,6 @@
     "datatype"
     "declare"
     "def"
-    "def_maps"
     "defaultsort"
     "defer"
     "defer_recdef"
@@ -67,8 +62,6 @@
     "done"
     "enable_pr"
     "end"
-    "end_import"
-    "end_setup"
     "exit"
     "extract"
     "extract_type"
@@ -78,7 +71,6 @@
     "fix"
     "fixpat"
     "fixrec"
-    "flush_dump"
     "from"
     "full_prf"
     "global"
@@ -86,9 +78,6 @@
     "header"
     "hence"
     "hide"
-    "ignore_thms"
-    "import_segment"
-    "import_theory"
     "inductive"
     "inductive_cases"
     "init_toplevel"
@@ -163,8 +152,6 @@
     "sect"
     "section"
     "setup"
-    "setup_dump"
-    "setup_theory"
     "show"
     "sorry"
     "specification"
@@ -182,8 +169,6 @@
     "theory"
     "thm"
     "thm_deps"
-    "thm_maps"
-    "thms_containing"
     "thus"
     "token_translation"
     "touch_all_thys"
@@ -193,7 +178,6 @@
     "txt"
     "txt_raw"
     "typ"
-    "type_maps"
     "typed_print_translation"
     "typedecl"
     "typedef"
@@ -208,6 +192,7 @@
     "use_thy"
     "use_thy_only"
     "using"
+    "value"
     "welcome"
     "with"
     "{"
@@ -333,7 +318,6 @@
     "term"
     "thm"
     "thm_deps"
-    "thms_containing"
     "touch_all_thys"
     "touch_child_thys"
     "touch_thy"
@@ -343,6 +327,7 @@
     "use"
     "use_thy"
     "use_thy_only"
+    "value"
     "welcome"))
 
 (defconst isar-keywords-theory-begin
@@ -362,7 +347,6 @@
 
 (defconst isar-keywords-theory-decl
   '("ML_setup"
-    "append_dump"
     "arities"
     "automaton"
     "axclass"
@@ -372,31 +356,21 @@
     "code_library"
     "code_module"
     "coinductive"
-    "const_maps"
-    "const_moves"
-    "const_renames"
     "constdefs"
     "consts"
     "consts_code"
     "datatype"
-    "def_maps"
     "defaultsort"
     "defer_recdef"
     "defs"
     "domain"
-    "end_import"
-    "end_setup"
     "extract"
     "extract_type"
     "finalconsts"
     "fixpat"
     "fixrec"
-    "flush_dump"
     "global"
     "hide"
-    "ignore_thms"
-    "import_segment"
-    "import_theory"
     "inductive"
     "judgment"
     "lemmas"
@@ -419,16 +393,12 @@
     "refute_params"
     "rep_datatype"
     "setup"
-    "setup_dump"
-    "setup_theory"
     "syntax"
     "text"
     "text_raw"
     "theorems"
-    "thm_maps"
     "token_translation"
     "translations"
-    "type_maps"
     "typed_print_translation"
     "typedecl"
     "types"