Theory AOT_commands

1(*<*)
2theory AOT_commands
3  imports AOT_model "HOL-Eisbach.Eisbach_Tools"
4  keywords "AOT_define" :: thy_decl
5       and "AOT_theorem" :: thy_goal
6       and "AOT_lemma" :: thy_goal
7       and "AOT_act_theorem" :: thy_goal
8       and "AOT_act_lemma" :: thy_goal
9
10       and "AOT_axiom" :: thy_goal
11       and "AOT_act_axiom" :: thy_goal
12
13       and "AOT_assume" :: prf_asm % "proof"
14       and "AOT_have" :: prf_goal % "proof"
15       and "AOT_hence" :: prf_goal % "proof"
16       and "AOT_modally_strict {" :: prf_open % "proof"
17       and "AOT_actually {" :: prf_open % "proof"
18       and "AOT_obtain" :: prf_asm_goal % "proof"
19       and "AOT_show" :: prf_asm_goal % "proof"
20       and "AOT_thus" :: prf_asm_goal % "proof"
21
22       and "AOT_find_theorems" :: diag
23       and "AOT_sledgehammer" :: diag
24       and "AOT_sledgehammer_only" :: diag
25       and "AOT_syntax_print_translations" :: thy_decl
26       and "AOT_no_syntax_print_translations" :: thy_decl
27begin
28(*>*)
29
30section‹Outer Syntax Commands›
31
32nonterminal AOT_prop
33nonterminal φ
34nonterminal φ'
35nonterminal τ
36nonterminal τ'
37nonterminal "AOT_axiom"
38nonterminal "AOT_act_axiom"
39ML_file AOT_keys.ML
40ML_file AOT_commands.ML
41setup‹AOT_Theorems.setup›
42setup‹AOT_Definitions.setup›
43setup‹AOT_no_atp.setup›
44
45(*<*)
46end
47(*>*)