--- a/record-ex.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/record-ex.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -1,8 +1,8 @@
 module record-ex where
 
 data _∨_  (A B : Set) : Set where
-      or1 : A -> A ∨ B
-      or2 : B -> A ∨ B
+      or1 : A → A ∨ B
+      or2 : B → A ∨ B
 
 postulate A B C : Set
 postulate a1 a2 a3 : A
@@ -13,7 +13,7 @@
 y : ( A ∨ B )
 y = or2 b1
 
-f : ( A ∨ B ) -> A
+f : ( A ∨ B ) → A
 f (or1 a) = a
 f (or2 b) = a1
 
@@ -39,7 +39,7 @@
 
 data Nat : Set where
    zero : Nat
-   suc  : Nat -> Nat
+   suc  : Nat → Nat
 
 record Mod3 (m : Nat) : Set where
    field
@@ -49,6 +49,6 @@
 
 open Mod3 
 
-Lemma1 :  ( x : Mod3 ( suc (suc (suc (suc zero))))) ( y : Mod3 ( suc zero ) ) -> n x  ≡ n y 
+Lemma1 :  ( x : Mod3 ( suc (suc (suc (suc zero))))) ( y : Mod3 ( suc zero ) ) → n x  ≡ n y 
 Lemma1 x y =  mod3 y