1Theory NumConvContext[bare] 2Ancestors 3 arithmetic 4Libs 5 HolKernel Parse boolLib 6 7Theorem save_zero: 8 NUMERAL ZERO = 0 9Proof 10 REWRITE_TAC [arithmeticTheory.NUMERAL_DEF, arithmeticTheory.ALT_ZERO] 11QED