src/HOL/Sum_Type.thy
changeset 10832 e33b47e4246d
parent 10213 01c2744a3786
child 11609 3f3d1add4d94
     1.1 --- a/src/HOL/Sum_Type.thy	Tue Jan 09 15:18:07 2001 +0100
     1.2 +++ b/src/HOL/Sum_Type.thy	Tue Jan 09 15:22:13 2001 +0100
     1.3 @@ -40,7 +40,7 @@
     1.4    Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
     1.5    Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
     1.6  
     1.7 -  sum_def       "A <+> B == (Inl``A) Un (Inr``B)"
     1.8 +  sum_def       "A <+> B == (Inl`A) Un (Inr`B)"
     1.9  
    1.10    (*for selecting out the components of a mutually recursive definition*)
    1.11    Part_def      "Part A h == A Int {x. ? z. x = h(z)}"