Session CTT
View
theory dependencies
View
document
View
outline
Theories
CTT
File ‹~~/src/Provers/typedsimp.ML›
File ‹rew.ML›
Typechecking
Elimination
Equality
Synthesis