equal
deleted
inserted
replaced
26 "apply" |
26 "apply" |
27 "apply_end" |
27 "apply_end" |
28 "assume" |
28 "assume" |
29 "atom_decl" |
29 "atom_decl" |
30 "attribute_setup" |
30 "attribute_setup" |
31 "ax_specification" |
|
32 "axiomatization" |
31 "axiomatization" |
33 "back" |
32 "back" |
34 "bnf" |
33 "bnf" |
35 "bnf_decl" |
34 "bnf_decl" |
36 "boogie_file" |
35 "boogie_file" |
241 "show" |
240 "show" |
242 "simproc_setup" |
241 "simproc_setup" |
243 "simps_of_case" |
242 "simps_of_case" |
244 "sledgehammer" |
243 "sledgehammer" |
245 "sledgehammer_params" |
244 "sledgehammer_params" |
|
245 "smt2_status" |
246 "smt_status" |
246 "smt_status" |
247 "smt2_status" |
|
248 "solve_direct" |
247 "solve_direct" |
249 "sorry" |
248 "sorry" |
250 "spark_end" |
249 "spark_end" |
251 "spark_open" |
250 "spark_open" |
252 "spark_open_siv" |
251 "spark_open_siv" |
445 "prop" |
444 "prop" |
446 "pwd" |
445 "pwd" |
447 "quickcheck" |
446 "quickcheck" |
448 "refute" |
447 "refute" |
449 "sledgehammer" |
448 "sledgehammer" |
|
449 "smt2_status" |
450 "smt_status" |
450 "smt_status" |
451 "smt2_status" |
|
452 "solve_direct" |
451 "solve_direct" |
453 "spark_status" |
452 "spark_status" |
454 "term" |
453 "term" |
455 "term_cartouche" |
454 "term_cartouche" |
456 "thm" |
455 "thm" |
595 |
594 |
596 (defconst isar-keywords-theory-script |
595 (defconst isar-keywords-theory-script |
597 '()) |
596 '()) |
598 |
597 |
599 (defconst isar-keywords-theory-goal |
598 (defconst isar-keywords-theory-goal |
600 '("ax_specification" |
599 '("bnf" |
601 "bnf" |
|
602 "code_pred" |
600 "code_pred" |
603 "corollary" |
601 "corollary" |
604 "cpodef" |
602 "cpodef" |
605 "free_constructors" |
603 "free_constructors" |
606 "function" |
604 "function" |