freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/word32.ma b/helm/software/matita/contribs/ng_assembly/freescale/word32.ma
index 2e0dd8bac54b6f8578ef738b5dbaf516c2c70c8b..0887f799148f14428e3e9202adac0047f3033a6e 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/word32.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/word32.ma
@@ -32,21 +32,6 @@ nrecord word32 : Type ≝
  w32l: word16
  }.
 
-(*ndefinition word32_ind : ΠP:word32 → Prop.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝
-λP:word32 → Prop.λf:Πw:word16.Πw1:word16.P (mk_word32 w w1).λdw:word32.
- match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ].
-
-ndefinition word32_rec : ΠP:word32 → Set.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝
-λP:word32 → Set.λf:Πw:word16.Πw1:word16.P (mk_word32 w w1).λdw:word32.
- match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ].
-
-ndefinition word32_rect : ΠP:word32 → Type.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝
-λP:word32 → Type.λf:Πw:word16.Πw1:word16.P (mk_word32 w w1).λdw:word32.
- match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ].
-
-ndefinition w32h ≝ λdw:word32.match dw with [ mk_word32 x _ ⇒ x ].
-ndefinition w32l ≝ λdw:word32.match dw with [ mk_word32 _ x ⇒ x ].*)
-
 (* \langle \rangle *)
 notation "〈x.y〉" non associative with precedence 80
  for @{ 'mk_word32 $x $y }.