Corrected associativity: must be to right, as the type dictatess
authorpaulson
Mon, 09 Sep 1996 11:08:01 +0200
changeset 1962 e60a230da179
parent 1961 d33a5d59a29a
child 1963 a4abf41134e2
Corrected associativity: must be to right, as the type dictatess
src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Sep 09 10:59:32 1996 +0200
+++ b/src/HOL/Set.thy	Mon Sep 09 11:08:01 1996 +0200
@@ -31,7 +31,7 @@
   Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
   inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
   inj_onto      :: ['a => 'b, 'a set] => bool
-  "``"          :: ['a => 'b, 'a set] => ('b set)   (infixl 90)
+  "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
   ":"           :: ['a, 'a set] => bool             (infixl 50) (*membership*)