equal
deleted
inserted
replaced
10 "\\.\\." |
10 "\\.\\." |
11 "ML" |
11 "ML" |
12 "ML_command" |
12 "ML_command" |
13 "ML_setup" |
13 "ML_setup" |
14 "ProofGeneral\\.call_atp" |
14 "ProofGeneral\\.call_atp" |
15 "ProofGeneral\\.context_thy_only" |
|
16 "ProofGeneral\\.inform_file_processed" |
15 "ProofGeneral\\.inform_file_processed" |
17 "ProofGeneral\\.inform_file_retracted" |
16 "ProofGeneral\\.inform_file_retracted" |
18 "ProofGeneral\\.kill_proof" |
17 "ProofGeneral\\.kill_proof" |
19 "ProofGeneral\\.process_pgip" |
18 "ProofGeneral\\.process_pgip" |
20 "ProofGeneral\\.redo" |
|
21 "ProofGeneral\\.restart" |
19 "ProofGeneral\\.restart" |
22 "ProofGeneral\\.try_context_thy_only" |
|
23 "ProofGeneral\\.undo" |
20 "ProofGeneral\\.undo" |
24 "abbreviation" |
21 "abbreviation" |
25 "also" |
22 "also" |
26 "apply" |
23 "apply" |
27 "apply_end" |
24 "apply_end" |
40 "chapter" |
37 "chapter" |
41 "class" |
38 "class" |
42 "class_deps" |
39 "class_deps" |
43 "classes" |
40 "classes" |
44 "classrel" |
41 "classrel" |
45 "clear_undos" |
|
46 "code_abstype" |
42 "code_abstype" |
47 "code_axioms" |
43 "code_axioms" |
48 "code_class" |
44 "code_class" |
49 "code_const" |
45 "code_const" |
50 "code_gen" |
46 "code_gen" |
51 "code_instance" |
47 "code_instance" |
52 "code_library" |
48 "code_library" |
53 "code_module" |
49 "code_module" |
54 "code_modulename" |
50 "code_modulename" |
55 "code_moduleprolog" |
51 "code_moduleprolog" |
|
52 "code_monad" |
56 "code_reserved" |
53 "code_reserved" |
57 "code_type" |
54 "code_type" |
58 "coinductive" |
55 "coinductive" |
59 "coinductive2" |
56 "coinductive2" |
60 "commit" |
57 "commit" |
272 "unchecked" |
269 "unchecked" |
273 "uses" |
270 "uses" |
274 "where")) |
271 "where")) |
275 |
272 |
276 (defconst isar-keywords-control |
273 (defconst isar-keywords-control |
277 '("ProofGeneral\\.context_thy_only" |
274 '("ProofGeneral\\.inform_file_processed" |
278 "ProofGeneral\\.inform_file_processed" |
|
279 "ProofGeneral\\.inform_file_retracted" |
275 "ProofGeneral\\.inform_file_retracted" |
280 "ProofGeneral\\.kill_proof" |
276 "ProofGeneral\\.kill_proof" |
281 "ProofGeneral\\.process_pgip" |
277 "ProofGeneral\\.process_pgip" |
282 "ProofGeneral\\.redo" |
|
283 "ProofGeneral\\.restart" |
278 "ProofGeneral\\.restart" |
284 "ProofGeneral\\.try_context_thy_only" |
|
285 "ProofGeneral\\.undo" |
279 "ProofGeneral\\.undo" |
286 "cannot_undo" |
280 "cannot_undo" |
287 "clear_undos" |
|
288 "exit" |
281 "exit" |
289 "init_toplevel" |
282 "init_toplevel" |
290 "kill" |
283 "kill" |
291 "quit" |
284 "quit" |
292 "redo" |
285 "redo" |
390 "code_instance" |
383 "code_instance" |
391 "code_library" |
384 "code_library" |
392 "code_module" |
385 "code_module" |
393 "code_modulename" |
386 "code_modulename" |
394 "code_moduleprolog" |
387 "code_moduleprolog" |
|
388 "code_monad" |
395 "code_reserved" |
389 "code_reserved" |
396 "code_type" |
390 "code_type" |
397 "coinductive" |
391 "coinductive" |
398 "coinductive2" |
392 "coinductive2" |
399 "constdefs" |
393 "constdefs" |