Update proving-metatheorems-solutions-odd-even-plus.elf (#39)

standardml · Apr 9, 2024 · 7cc2c4e · 7cc2c4e
1 parent 2a3d841
commit 7cc2c4e
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/wiki/pages/proving-metatheorems-solutions-odd-even-plus.elf b/wiki/pages/proving-metatheorems-solutions-odd-even-plus.elf
@@ -171,7 +171,7 @@ soe : sum-odd-even
 
 The most straightforward approach here reuses [`succ-odd` from Exercise 3](/wiki/proving-metatheorems-solutions-odd-even-succ/) in exactly the same way as the "expected" solution to the previous theorem reused `succ-even`.
 
-First, we'll 
+First, we'll repeat the proof of `succ-odd` from Exercise 3:
 !}%
 
 succ-odd : odd N -> even (s N) -> type.
@@ -200,4 +200,4 @@ EvenN3)
 
 %worlds () (sum-odds _ _ _ _).
 %total D (sum-odds D _ _ _).
-%{!! end checked !!}%
+%{!! end checked !!}%