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