src/HOL/Library/Old_Datatype.thy
changeset 61952 546958347e05
parent 61943 7fba644ed827
child 62145 5b946c81dfbf
     1.1 --- a/src/HOL/Library/Old_Datatype.thy	Mon Dec 28 16:34:26 2015 +0100
     1.2 +++ b/src/HOL/Library/Old_Datatype.thy	Mon Dec 28 17:43:30 2015 +0100
     1.3 @@ -76,7 +76,7 @@
     1.4    In1_def:    "In1(M) == Scons (Numb 1) M"
     1.5  
     1.6    (*Function spaces*)
     1.7 -  Lim_def: "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}"
     1.8 +  Lim_def: "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}"
     1.9  
    1.10    (*the set of nodes with depth less than k*)
    1.11    ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"