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