From 98598bffa1cd21a05975eeab97f8a8baba1eb1ad Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Wed, 20 Dec 2023 13:39:29 +0000 Subject: [PATCH] oh I'm a fool, original lemmatab was better --- Game/Levels/Implication/L10one_ne_zero.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Game/Levels/Implication/L10one_ne_zero.lean b/Game/Levels/Implication/L10one_ne_zero.lean index 0cb7155..5464f1f 100644 --- a/Game/Levels/Implication/L10one_ne_zero.lean +++ b/Game/Levels/Implication/L10one_ne_zero.lean @@ -3,7 +3,7 @@ World "Implication" Level 10 Title "1 ≠ 0" -LemmaTab "Peano" +LemmaTab "012" namespace MyNat