src/HOL/Sum_Type.thy
changeset 22838 466599ecf610
parent 22622 25693088396b
child 25534 d0b74fdd6067
     1.1 --- a/src/HOL/Sum_Type.thy	Sun May 06 18:07:06 2007 +0200
     1.2 +++ b/src/HOL/Sum_Type.thy	Sun May 06 21:49:23 2007 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  global
     1.5  
     1.6  typedef (Sum)
     1.7 -  ('a, 'b) "+"          (infixr 10)
     1.8 +  ('a, 'b) "+"          (infixr "+" 10)
     1.9      = "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}"
    1.10    by auto
    1.11