1) added a function to retrieve all the universes currently in use

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/prod.ma b/helm/software/matita/contribs/ng_assembly/freescale/prod.ma
index 081d43408256d5a69af5924efa008a5c302ae63f..48d054d3a501fba7b682dde0d815938724fea97f 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/freescale/prod.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/prod.ma
@@ -13,15 +13,11 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
-(*                           Progetto FreeScale                           *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
+(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
 (*                                                                        *)
-(* Questo materiale fa parte della tesi:                                  *)
-(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
-(*                                                                        *)
-(*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
 include "freescale/bool.ma".
@@ -171,7 +167,7 @@ ndefinition eq_quadruple ≝
 ninductive Prod5T (T1:Type) (T2:Type) (T3:Type) (T4:Type) (T5:Type) : Type ≝
 quintuple : T1 → T2 → T3 → T4 → T5 → Prod5T T1 T2 T3 T4 T5.
 
-ndefinition Pro54T_ind
+ndefinition Prod5T_ind
  : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Prop.
    (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
    Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
@@ -180,7 +176,7 @@ ndefinition Pro54T_ind
 λp:Prod5T T1 T2 T3 T4 T5.
  match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
 
-ndefinition Pro54T_rec
+ndefinition Prod5T_rec
  : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Set.
    (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
    Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
@@ -189,7 +185,7 @@ ndefinition Pro54T_rec
 λp:Prod5T T1 T2 T3 T4 T5.
  match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
 
-ndefinition Pro54T_rect
+ndefinition Prod5T_rect
  : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Type.
    (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
    Πp:Prod5T T1 T2 T3 T4 T5.P p ≝