src/HOL/Sum.thy
changeset 1558 9c6ebfab4e05
parent 1515 4ed79ebab64d
child 2212 bd705e9de196
     1.1 --- a/src/HOL/Sum.thy	Wed Mar 06 14:19:39 1996 +0100
     1.2 +++ b/src/HOL/Sum.thy	Fri Mar 08 13:11:09 1996 +0100
     1.3 @@ -10,13 +10,12 @@
     1.4  
     1.5  (* type definition *)
     1.6  
     1.7 -consts
     1.8 +constdefs
     1.9    Inl_Rep       :: ['a, 'a, 'b, bool] => bool
    1.10 -  Inr_Rep       :: ['b, 'a, 'b, bool] => bool
    1.11 +  "Inl_Rep == (%a. %x y p. x=a & p)"
    1.12  
    1.13 -defs
    1.14 -  Inl_Rep_def   "Inl_Rep == (%a. %x y p. x=a & p)"
    1.15 -  Inr_Rep_def   "Inr_Rep == (%b. %x y p. y=b & ~p)"
    1.16 +  Inr_Rep       :: ['b, 'a, 'b, bool] => bool
    1.17 +  "Inr_Rep == (%b. %x y p. y=b & ~p)"
    1.18  
    1.19  typedef (Sum)
    1.20    ('a, 'b) "+"          (infixr 10)