src/HOL/Univ.thy
changeset 1384 007ad29ce6ca
parent 1370 7361ac9b024d
child 1396 48bcde67391b
     1.1 --- a/src/HOL/Univ.thy	Fri Dec 01 13:54:27 1995 +0100
     1.2 +++ b/src/HOL/Univ.thy	Fri Dec 01 14:17:50 1995 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4    'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
     1.5  
     1.6  types
     1.7 -  'a item = "'a node set"
     1.8 +  'a item = 'a node set
     1.9  
    1.10  consts
    1.11    Least     :: (nat=>bool) => nat    (binder "LEAST " 10)