etc/isar-keywords.el
changeset 41564 1cbf33a4406a
parent 41530 c7e14c8088a6
child 42356 e8777e3ea6ef
     1.1 --- a/etc/isar-keywords.el	Sat Jan 15 12:41:07 2011 +0100
     1.2 +++ b/etc/isar-keywords.el	Sat Jan 15 12:42:19 2011 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  ;;
     1.5  ;; Keyword classification tables for Isabelle/Isar.
     1.6 -;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Nominal + HOL-Statespace.
     1.7 +;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Nominal + HOL-Statespace + HOL-SPARK.
     1.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     1.9  ;;
    1.10  
    1.11 @@ -223,6 +223,11 @@
    1.12      "smt_status"
    1.13      "solve_direct"
    1.14      "sorry"
    1.15 +    "spark_end"
    1.16 +    "spark_open"
    1.17 +    "spark_proof_functions"
    1.18 +    "spark_status"
    1.19 +    "spark_vc"
    1.20      "specification"
    1.21      "statespace"
    1.22      "subclass"
    1.23 @@ -399,6 +404,7 @@
    1.24      "sledgehammer"
    1.25      "smt_status"
    1.26      "solve_direct"
    1.27 +    "spark_status"
    1.28      "term"
    1.29      "thm"
    1.30      "thm_deps"
    1.31 @@ -511,6 +517,9 @@
    1.32      "setup"
    1.33      "simproc_setup"
    1.34      "sledgehammer_params"
    1.35 +    "spark_end"
    1.36 +    "spark_open"
    1.37 +    "spark_proof_functions"
    1.38      "statespace"
    1.39      "syntax"
    1.40      "syntax_declaration"
    1.41 @@ -551,6 +560,7 @@
    1.42      "schematic_corollary"
    1.43      "schematic_lemma"
    1.44      "schematic_theorem"
    1.45 +    "spark_vc"
    1.46      "specification"
    1.47      "subclass"
    1.48      "sublocale"