update un delayed_updating

[helm.git] / matita / matita / nlibrary / datatypes / bool.ma

diff --git a/matita/matita/nlibrary/datatypes/bool.ma b/matita/matita/nlibrary/datatypes/bool.ma
index eda979d69b3c1121e76dadec86b5c789f8559086..044296559e674b0d1dce25b88b8e540fbaac74dc 100644 (file)
--- a/matita/matita/nlibrary/datatypes/bool.ma
+++ b/matita/matita/nlibrary/datatypes/bool.ma
@@ -14,9 +14,9 @@
 
 include "logic/pts.ma".
 
-ninductive bool: Type[0] ≝ true: bool | false: bool.
+inductive bool: Type[0] ≝ true: bool | false: bool.
  
-ndefinition orb ≝ λa,b:bool. match a with [ true ⇒ true | _ ⇒ b ].
+definition orb ≝ λa,b:bool. match a with [ true ⇒ true | _ ⇒ b ].
 
 notation "a || b" left associative with precedence 30 for @{'orb $a $b}.
 interpretation "orb" 'orb a b = (orb a b).
\ No newline at end of file