src/HOL/Sum.thy
changeset 1370 7361ac9b024d
parent 1151 c820b3cc3df0
child 1423 5726a8243d3f
     1.1 --- a/src/HOL/Sum.thy	Mon Nov 27 13:44:56 1995 +0100
     1.2 +++ b/src/HOL/Sum.thy	Wed Nov 29 16:44:59 1995 +0100
     1.3 @@ -11,8 +11,8 @@
     1.4  (* type definition *)
     1.5  
     1.6  consts
     1.7 -  Inl_Rep       :: "['a, 'a, 'b, bool] => bool"
     1.8 -  Inr_Rep       :: "['b, 'a, 'b, bool] => bool"
     1.9 +  Inl_Rep       :: ['a, 'a, 'b, bool] => bool
    1.10 +  Inr_Rep       :: ['b, 'a, 'b, bool] => bool
    1.11  
    1.12  defs
    1.13    Inl_Rep_def   "Inl_Rep == (%a. %x y p. x=a & p)"
    1.14 @@ -32,7 +32,7 @@
    1.15  
    1.16    (*disjoint sum for sets; the operator + is overloaded with wrong type!*)
    1.17    "plus"        :: "['a set, 'b set] => ('a + 'b) set"        (infixr 65)
    1.18 -  Part          :: "['a set, 'b => 'a] => 'a set"
    1.19 +  Part          :: ['a set, 'b => 'a] => 'a set
    1.20  
    1.21  translations
    1.22    "case p of Inl(x) => a | Inr(y) => b" == "sum_case (%x.a) (%y.b) p"