equal
deleted
inserted
replaced
1 ;; |
1 ;; |
2 ;; Keyword classification tables for Isabelle/Isar. |
2 ;; Keyword classification tables for Isabelle/Isar. |
3 ;; Generated from HOL + Pure + Pure-ProofGeneral + HOL-Command. |
3 ;; Generated from Pure + HOL + Pure-ProofGeneral + HOL-Nominal-Prove. |
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 '("\\." |
9 "\\.\\." |
9 "\\.\\." |
10 "Isabelle\\.command" |
10 "Isabelle\\.command" |
11 "Isar\\.begin_document" |
11 "Isar\\.begin_document" |
12 "Isar\\.command" |
|
13 "Isar\\.define_command" |
12 "Isar\\.define_command" |
14 "Isar\\.edit_document" |
13 "Isar\\.edit_document" |
15 "Isar\\.end_document" |
14 "Isar\\.end_document" |
16 "Isar\\.insert" |
|
17 "Isar\\.remove" |
|
18 "ML" |
15 "ML" |
19 "ML_command" |
16 "ML_command" |
20 "ML_prf" |
17 "ML_prf" |
21 "ML_val" |
18 "ML_val" |
22 "ProofGeneral\\.inform_file_processed" |
19 "ProofGeneral\\.inform_file_processed" |
182 "pwd" |
179 "pwd" |
183 "qed" |
180 "qed" |
184 "quickcheck" |
181 "quickcheck" |
185 "quickcheck_params" |
182 "quickcheck_params" |
186 "quit" |
183 "quit" |
|
184 "quotient" |
187 "realizability" |
185 "realizability" |
188 "realizers" |
186 "realizers" |
189 "recdef" |
187 "recdef" |
190 "recdef_tc" |
188 "recdef_tc" |
191 "record" |
189 "record" |
284 "where")) |
282 "where")) |
285 |
283 |
286 (defconst isar-keywords-control |
284 (defconst isar-keywords-control |
287 '("Isabelle\\.command" |
285 '("Isabelle\\.command" |
288 "Isar\\.begin_document" |
286 "Isar\\.begin_document" |
289 "Isar\\.command" |
|
290 "Isar\\.define_command" |
287 "Isar\\.define_command" |
291 "Isar\\.edit_document" |
288 "Isar\\.edit_document" |
292 "Isar\\.end_document" |
289 "Isar\\.end_document" |
293 "Isar\\.insert" |
|
294 "Isar\\.remove" |
|
295 "ProofGeneral\\.inform_file_processed" |
290 "ProofGeneral\\.inform_file_processed" |
296 "ProofGeneral\\.inform_file_retracted" |
291 "ProofGeneral\\.inform_file_retracted" |
297 "ProofGeneral\\.kill_proof" |
292 "ProofGeneral\\.kill_proof" |
298 "ProofGeneral\\.process_pgip" |
293 "ProofGeneral\\.process_pgip" |
299 "ProofGeneral\\.restart" |
294 "ProofGeneral\\.restart" |
485 "function" |
480 "function" |
486 "instance" |
481 "instance" |
487 "interpretation" |
482 "interpretation" |
488 "lemma" |
483 "lemma" |
489 "prove" |
484 "prove" |
|
485 "quotient" |
490 "recdef_tc" |
486 "recdef_tc" |
491 "rep_datatype" |
487 "rep_datatype" |
492 "specification" |
488 "specification" |
493 "subclass" |
489 "subclass" |
494 "sublocale" |
490 "sublocale" |