Session Metalogic_ProofChecker
View
theory dependencies
View
document
View
outline
Theories
Core
List-Index.List_Index
HOL-Library.AList
HOL-Library.Sublist
HOL-Eisbach.Eisbach
File ‹parse_tools.ML›
File ‹method_closure.ML›
File ‹eisbach_rule_insts.ML›
File ‹match_method.ML›
HOL-Library.Case_Converter
File ‹case_converter.ML›
HOL-Library.Simps_Case_Conv
File ‹simps_case_conv.ML›
Preliminaries
Term
Sorts
SortConstants
Theory
Term_Subst
HOL-Library.Char_ord
Name
BetaNorm
BetaNormProof
EtaNorm
EtaNormProof
Logic
EqualityProof
ProofTerm
SortsExe
Instances
TheoryExe
CheckerExe
HOL-Library.Code_Target_Int
HOL-Library.Code_Abstract_Nat
HOL-Library.Code_Target_Nat
CodeGen