freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/model.ma b/helm/software/matita/contribs/ng_assembly/freescale/model.ma
index 5dad70809d036fb226473c97bbfbd39093b9d8fe..adafa40f3f3e59ac6e3f6cccc753b3fc557e4eea 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/model.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/model.ma
@@ -31,18 +31,6 @@ ninductive HC05_mcu_model : Type ≝
   MC68HC05J5A: HC05_mcu_model
   (*..*).
 
-ndefinition HC05_mcu_model_ind : ΠP:HC05_mcu_model → Prop.P MC68HC05J5A → Πh:HC05_mcu_model.P h ≝
-λP:HC05_mcu_model → Prop.λp:P MC68HC05J5A.λh:HC05_mcu_model.
- match h with [ MC68HC05J5A ⇒ p ].
-
-ndefinition HC05_mcu_model_rec : ΠP:HC05_mcu_model → Set.P MC68HC05J5A → Πh:HC05_mcu_model.P h ≝
-λP:HC05_mcu_model → Set.λp:P MC68HC05J5A.λh:HC05_mcu_model.
- match h with [ MC68HC05J5A ⇒ p ].
-
-ndefinition HC05_mcu_model_rect : ΠP:HC05_mcu_model → Type.P MC68HC05J5A → Πh:HC05_mcu_model.P h ≝
-λP:HC05_mcu_model → Type.λp:P MC68HC05J5A.λh:HC05_mcu_model.
- match h with [ MC68HC05J5A ⇒ p ].
-
 (* modelli di HC08 *)
 ninductive HC08_mcu_model : Type ≝
   MC68HC08AB16A: HC08_mcu_model