Release 0.5.9.

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

diff --git a/helm/software/matita/nlibrary/datatypes/bool.ma b/helm/software/matita/nlibrary/datatypes/bool.ma
index eda979d69b3c1121e76dadec86b5c789f8559086..be42b597a5abd471a2000a85272ecb12d50d06fe 100644 (file)
--- a/helm/software/matita/nlibrary/datatypes/bool.ma
+++ b/helm/software/matita/nlibrary/datatypes/bool.ma
@@ -14,9 +14,6 @@
 
 include "logic/pts.ma".
 
-ninductive bool: Type[0] ≝ true: bool | false: bool.
- 
-ndefinition 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
+ninductive bool: Type[0] ≝
+   true: bool
+ | false: bool.
\ No newline at end of file