freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / bool.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/bool.ma b/helm/software/matita/contribs/ng_assembly/freescale/bool.ma
index 7f7dba743ba4dc0d834daec205e722f530c0307b..e7ea4dcfa875289aa285af631309dba2fa1fc175 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/bool.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/bool.ma
@@ -30,18 +30,6 @@ ninductive bool : Type ≝
   true : bool
 | false : bool.
 
-ndefinition bool_ind : ΠP:bool → Prop.P true → P false → Πb:bool.P b ≝
-λP:bool → Prop.λp:P true.λp1:P false.λb:bool.
- match b with [ true ⇒ p | false ⇒ p1 ].
-
-ndefinition bool_rec : ΠP:bool → Set.P true → P false → Πb:bool.P b ≝
-λP:bool → Set.λp:P true.λp1:P false.λb:bool.
- match b with [ true ⇒ p | false ⇒ p1 ].
-
-ndefinition bool_rect : ΠP:bool → Type.P true → P false → Πb:bool.P b ≝
-λP:bool → Type.λp:P true.λp1:P false.λb:bool.
- match b with [ true ⇒ p | false ⇒ p1 ].
-
 (* operatori booleani *)
 
 ndefinition eq_bool ≝