X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Ftheory.ma;h=a9e6287a8a074741fd7a3f140f01b3b7120cb004;hb=dcde2b362a4106e36623d25e6a2d26dffac61848;hp=81422d2041dd0e9ba3184f4cc495cebf69aad800;hpb=633b66b935bbc2c38a5abc2be958359335123258;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
index 81422d204..a9e6287a8 100644
--- a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
@@ -59,14 +59,15 @@ interpretation "logical and" 'and x y = (And x y).
 
 nlemma proj1: ∀A,B:Prop.A ∧ B → A.
  #A; #B; #H;
- napply (And_ind A B ?? H);
+ (* \ldots al posto di ??? *)
+ napply (And_ind A B … H);
  #H1; #H2;
  napply H1.
 nqed.
 
 nlemma proj2: ∀A,B:Prop.A ∧ B → B.
  #A; #B; #H;
- napply (And_ind A B ?? H);
+ napply (And_ind A B … H);
  #H1; #H2;
  napply H2.
 nqed.
@@ -88,7 +89,7 @@ ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
 
 ndefinition iff ≝
-λA,B.(A -> B) ∧ (B -> A).
+λA,B.(A → B) ∧ (B → A).
 
 (* higher_order_defs/relations *)
 
@@ -130,12 +131,12 @@ nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
  nnormalize;
  #x; #y; #H;
  nrewrite < H;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
  #A; #x; #P; #H; #y; #H1;
- nrewrite < (symmetric_eq ??? H1);
+ nrewrite < (symmetric_eq … H1);
  napply H.
 nqed.
 
@@ -152,12 +153,12 @@ ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
 
 ninductive list (A:Type) : Type ≝
   nil: list A
-| cons: A -> list A -> list A.
+| cons: A → list A → list A.
 
 nlet rec append A (l1: list A) l2 on l1 ≝
  match l1 with
-  [ nil => l2
-  | (cons hd tl) => cons A hd (append A tl l2) ].
+  [ nil ⇒ l2
+  | (cons hd tl) ⇒ cons A hd (append A tl l2) ].
 
 notation "hvbox(hd break :: tl)"
   right associative with precedence 47
@@ -180,7 +181,7 @@ nlemma list_destruct_1 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x
  nchange with (match cons T x2 y2 with [ nil ⇒ False | cons a _ ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → y1 = y2.
@@ -188,7 +189,7 @@ nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x
  nchange with (match cons T x2 y2 with [ nil ⇒ False | cons _ b ⇒ y1 = b ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
@@ -208,12 +209,13 @@ nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → F
 nqed.
 
 nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
- #T; #l; nelim l;
+ #T; #l;
+ nelim l;
  nnormalize;
- ##[ ##1: napply (refl_eq ??)
+ ##[ ##1: napply refl_eq
  ##| ##2: #x; #y; #H;
           nrewrite > H;
-          napply (refl_eq ??)
+          napply refl_eq
  ##]
 nqed.
 
@@ -221,22 +223,22 @@ nlemma associative_list : ∀T.associative (list T) (append T).
  #T; #x; #y; #z;
  nelim x;
  nnormalize;
- ##[ ##1: napply (refl_eq ??)
+ ##[ ##1: napply refl_eq
  ##| ##2: #a; #b; #H;
           nrewrite > H;
-          napply (refl_eq ??)
+          napply refl_eq
  ##]
 nqed.
 
 nlemma cons_append_commute : ∀T:Type.∀l1,l2:list T.∀a:T.a :: (l1 @ l2) = (a :: l1) @ l2.
  #T; #l1; #l2; #a;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
  #T; #a; #l; #l1;
  nrewrite > (associative_list T l [a] l1);
  nnormalize;
- napply (refl_eq ??).
-nqed.
\ No newline at end of file
+ napply refl_eq.
+nqed.