Session Proof_Strategy_Language
View
theory dependencies
View
document
View
outline
Theories
Try_Hard
File ‹Utils.ML›
File ‹Subtool.ML›
File ‹Dynamic_Tactic_Generation.ML›
File ‹Constructor_Class.ML›
File ‹Instantiation.ML›
File ‹Monadic_Prover.ML›
File ‹Parser_Combinator.ML›
File ‹PSL_Parser.ML›
File ‹Isar_Interface.ML›
PSL
HOL-Eisbach.Eisbach
File ‹parse_tools.ML›
File ‹method_closure.ML›
File ‹eisbach_rule_insts.ML›
File ‹match_method.ML›
Example