src/HOL/Sum.thy
changeset 3842 b55686a7b22c
parent 2983 f914a1663b2a
child 3947 eb707467f8c5
     1.1 --- a/src/HOL/Sum.thy	Fri Oct 10 18:37:49 1997 +0200
     1.2 +++ b/src/HOL/Sum.thy	Fri Oct 10 19:02:28 1997 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4    Part          :: ['a set, 'b => 'a] => 'a set
     1.5  
     1.6  translations
     1.7 -  "case p of Inl x => a | Inr y => b" == "sum_case (%x.a) (%y.b) p"
     1.8 +  "case p of Inl x => a | Inr y => b" == "sum_case (%x. a) (%y. b) p"
     1.9  
    1.10  defs
    1.11    Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"