Entry	Value
Package Name	natural-exp-def
Count	2
Theorems	EXP_0 : !m. m EXP 0 = 1 EXP_SUC : !m n. m EXP SUC n = m * m EXP n

Back to main package page