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 45attribute_setup AOT_elim = ‹ 46Args.term >> 47(fn (Const (name, _)) => Thm.declaration_attribute (fn thm => Context.mapping (AOT_RulifyElims.map (Symtab.map_default (name,[]) (fn thms => thm::thms))) I)) 48› 49attribute_setup AOT_inst = ‹ 50Args.term >> 51(fn (Const (name, _)) => Thm.declaration_attribute (fn thm => Context.mapping (AOT_RulifyInsts.map (Symtab.update_new (name,thm))) I)) 52› 53attribute_setup AOT_intro = ‹ 54Scan.succeed 55(Thm.declaration_attribute (fn thm => Context.mapping (AOT_RulifyIntros.map (Net.insert (K true) (Net.key_of_term (Thm.concl_of thm), thm))) I)) 56› 57 58(*<*) 59end 60(*>*)