Patch by Ferruccio that enables \top/\bot for False/True undone.

[helm.git] / matita / matita / lib / arithmetics / nat.ma

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 76ccbd5cc48cc3c169fedd0f86ae6567bf68cf00..81d6c9310247dc42c5f2d0d76e66a986ae1d45fc 100644 (file)
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -27,7 +27,7 @@ definition pred ≝
  λn. match n with [ O ⇒ O | S p ⇒ p].
 
 definition not_zero: nat → Prop ≝
- λn: nat. match n with [ O ⇒ ⊥ | (S p) ⇒ ⊤ ].
+ λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ].
 
 (* order relations *)