freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
index 9679d66ed85cdfb692ec2cc26156cbb71cc4b99e..a9e6287a8a074741fd7a3f140f01b3b7120cb004 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
@@ -59,6 +59,7 @@ interpretation "logical and" 'and x y = (And x y).
 
 nlemma proj1: ∀A,B:Prop.A ∧ B → A.
  #A; #B; #H;
+ (* \ldots al posto di ??? *)
  napply (And_ind A B … H);
  #H1; #H2;
  napply H1.
@@ -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 *)
 
@@ -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