# HG changeset patch
# User berghofe
# Date 1295091739 -3600
# Node ID 1cbf33a4406a2d197024ff0c4864618fc5c7958b
# Parent  0b0cec12aae3a027f3b4a79c8b2ca717cd9f783c
Include HOL-SPARK keywords

diff -r 0b0cec12aae3 -r 1cbf33a4406a etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sat Jan 15 12:41:07 2011 +0100
+++ b/etc/isar-keywords.el	Sat Jan 15 12:42:19 2011 +0100
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Nominal + HOL-Statespace.
+;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Nominal + HOL-Statespace + HOL-SPARK.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
@@ -223,6 +223,11 @@
     "smt_status"
     "solve_direct"
     "sorry"
+    "spark_end"
+    "spark_open"
+    "spark_proof_functions"
+    "spark_status"
+    "spark_vc"
     "specification"
     "statespace"
     "subclass"
@@ -399,6 +404,7 @@
     "sledgehammer"
     "smt_status"
     "solve_direct"
+    "spark_status"
     "term"
     "thm"
     "thm_deps"
@@ -511,6 +517,9 @@
     "setup"
     "simproc_setup"
     "sledgehammer_params"
+    "spark_end"
+    "spark_open"
+    "spark_proof_functions"
     "statespace"
     "syntax"
     "syntax_declaration"
@@ -551,6 +560,7 @@
     "schematic_corollary"
     "schematic_lemma"
     "schematic_theorem"
+    "spark_vc"
     "specification"
     "subclass"
     "sublocale"