Session Case_Labeling
View
theory dependencies
View
document
View
outline
Theories
Case_Labeling
File ‹print_nested_cases.ML›
File ‹util.ML›
File ‹casify.ML›
HOL-Hoare.Hoare_Syntax
File ‹hoare_syntax.ML›
HOL-Hoare.Hoare_Tac
File ‹hoare_tac.ML›
HOL-Hoare.Hoare_Logic
Labeled_Hoare
File ‹labeled_hoare_tac.ML›
HOL-Hoare.Arith2
Labeled_Hoare_Examples
HOL-Eisbach.Eisbach
File ‹parse_tools.ML›
File ‹method_closure.ML›
File ‹eisbach_rule_insts.ML›
File ‹match_method.ML›
Conditionals
Monadic_Language
File ‹$AFP/Case_Labeling/util.ML›
Case_Labeling_Examples