equal
deleted
inserted
replaced
1 ;; |
1 ;; |
2 ;; Keyword classification tables for Isabelle/Isar. |
2 ;; Keyword classification tables for Isabelle/Isar. |
3 ;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Nominal + HOL-Statespace. |
3 ;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Nominal + HOL-Statespace + HOL-SPARK. |
4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** |
4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** |
5 ;; |
5 ;; |
6 |
6 |
7 (defconst isar-keywords-major |
7 (defconst isar-keywords-major |
8 '("\\." |
8 '("\\." |
221 "sledgehammer" |
221 "sledgehammer" |
222 "sledgehammer_params" |
222 "sledgehammer_params" |
223 "smt_status" |
223 "smt_status" |
224 "solve_direct" |
224 "solve_direct" |
225 "sorry" |
225 "sorry" |
|
226 "spark_end" |
|
227 "spark_open" |
|
228 "spark_proof_functions" |
|
229 "spark_status" |
|
230 "spark_vc" |
226 "specification" |
231 "specification" |
227 "statespace" |
232 "statespace" |
228 "subclass" |
233 "subclass" |
229 "sublocale" |
234 "sublocale" |
230 "subsect" |
235 "subsect" |
397 "quickcheck" |
402 "quickcheck" |
398 "refute" |
403 "refute" |
399 "sledgehammer" |
404 "sledgehammer" |
400 "smt_status" |
405 "smt_status" |
401 "solve_direct" |
406 "solve_direct" |
|
407 "spark_status" |
402 "term" |
408 "term" |
403 "thm" |
409 "thm" |
404 "thm_deps" |
410 "thm_deps" |
405 "thy_deps" |
411 "thy_deps" |
406 "try" |
412 "try" |
509 "record" |
515 "record" |
510 "refute_params" |
516 "refute_params" |
511 "setup" |
517 "setup" |
512 "simproc_setup" |
518 "simproc_setup" |
513 "sledgehammer_params" |
519 "sledgehammer_params" |
|
520 "spark_end" |
|
521 "spark_open" |
|
522 "spark_proof_functions" |
514 "statespace" |
523 "statespace" |
515 "syntax" |
524 "syntax" |
516 "syntax_declaration" |
525 "syntax_declaration" |
517 "text" |
526 "text" |
518 "text_raw" |
527 "text_raw" |
549 "recdef_tc" |
558 "recdef_tc" |
550 "rep_datatype" |
559 "rep_datatype" |
551 "schematic_corollary" |
560 "schematic_corollary" |
552 "schematic_lemma" |
561 "schematic_lemma" |
553 "schematic_theorem" |
562 "schematic_theorem" |
|
563 "spark_vc" |
554 "specification" |
564 "specification" |
555 "subclass" |
565 "subclass" |
556 "sublocale" |
566 "sublocale" |
557 "termination" |
567 "termination" |
558 "theorem" |
568 "theorem" |