(*<*)
theory AOT_commands
  imports AOT_model "HOL-Eisbach.Eisbach_Tools"
  keywords "AOT_define" :: thy_decl
       and "AOT_theorem" :: thy_goal
       and "AOT_lemma" :: thy_goal
       and "AOT_act_theorem" :: thy_goal
       and "AOT_act_lemma" :: thy_goal

       and "AOT_axiom" :: thy_goal
       and "AOT_act_axiom" :: thy_goal

       and "AOT_assume" :: prf_asm % "proof"
       and "AOT_have" :: prf_goal % "proof"
       and "AOT_hence" :: prf_goal % "proof"
       and "AOT_modally_strict {" :: prf_open % "proof"
       and "AOT_actually {" :: prf_open % "proof"
       and "AOT_obtain" :: prf_asm_goal % "proof"
       and "AOT_show" :: prf_asm_goal % "proof"
       and "AOT_thus" :: prf_asm_goal % "proof"

       and "AOT_find_theorems" :: diag
       and "AOT_sledgehammer" :: diag
       and "AOT_sledgehammer_only" :: diag
       and "AOT_syntax_print_translations" :: thy_decl
       and "AOT_no_syntax_print_translations" :: thy_decl
begin
(*>*)

section‹Outer Syntax Commands›

nonterminal AOT_prop
nonterminal φ
nonterminal φ'
nonterminal τ
nonterminal τ'
nonterminal "AOT_axiom"
nonterminal "AOT_act_axiom"
ML_file AOT_keys.ML
ML_file AOT_commands.ML
setup‹AOT_Theorems.setup›
setup‹AOT_Definitions.setup›
setup‹AOT_no_atp.setup›

(*<*)
end
(*>*)