# HG changeset patch
# User lcp
# Date 797158401 -7200
# Node ID 9bf3816298d0cab0dc314ae00b3b74821fdedc21
# Parent  91d09e2627994629ff89ab67ef28ee0a5406d526
Gave tighter priorities to SUM and PROD to reduce ambiguities.

diff -r 91d09e262799 -r 9bf3816298d0 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Thu Apr 06 10:51:42 1995 +0200
+++ b/src/CCL/Type.thy	Thu Apr 06 10:53:21 1995 +0200
@@ -14,24 +14,28 @@
   Subtype       :: "['a set, 'a => o] => 'a set"
   Bool          :: "i set"
   Unit          :: "i set"
-  "+"           :: "[i set, i set] => i set"            (infixr 55)
+  "+"           :: "[i set, i set] => i set"         (infixr 55)
   Pi            :: "[i set, i => i set] => i set"
   Sigma         :: "[i set, i => i set] => i set"
   Nat           :: "i set"
   List          :: "i set => i set"
   Lists         :: "i set => i set"
   ILists        :: "i set => i set"
-  TAll          :: "(i set => i set) => i set"          (binder "TALL " 55)
-  TEx           :: "(i set => i set) => i set"          (binder "TEX " 55)
-  Lift          :: "i set => i set"                     ("(3[_])")
+  TAll          :: "(i set => i set) => i set"       (binder "TALL " 55)
+  TEx           :: "(i set => i set) => i set"       (binder "TEX " 55)
+  Lift          :: "i set => i set"                  ("(3[_])")
 
   SPLIT         :: "[i, [i, i] => i set] => i set"
 
-  "@Pi"         :: "[idt, i set, i set] => i set"       ("(3PROD _:_./ _)" [] 60)
-  "@Sigma"      :: "[idt, i set, i set] => i set"       ("(3SUM _:_./ _)" [] 60)
-  "@->"         :: "[i set, i set] => i set"            ("(_ ->/ _)"  [54, 53] 53)
-  "@*"          :: "[i set, i set] => i set"            ("(_ */ _)" [56, 55] 55)
-  "@Subtype"    :: "[idt, 'a set, o] => 'a set"         ("(1{_: _ ./ _})")
+  "@Pi"         :: "[idt, i set, i set] => i set"    ("(3PROD _:_./ _)"
+  				[0,0,60] 60)
+
+  "@Sigma"      :: "[idt, i set, i set] => i set"    ("(3SUM _:_./ _)"
+  				[0,0,60] 60)
+  
+  "@->"         :: "[i set, i set] => i set"         ("(_ ->/ _)"  [54, 53] 53)
+  "@*"          :: "[i set, i set] => i set"         ("(_ */ _)" [56, 55] 55)
+  "@Subtype"    :: "[idt, 'a set, o] => 'a set"      ("(1{_: _ ./ _})")
 
 translations
   "PROD x:A. B" => "Pi(A, %x. B)"