Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Tools/holcf_library.ML
changeset 35906 e0382e4b4da7
parent 35785 cdaf99fddd17
child 35912 b0e300bd3a2c
equal deleted inserted replaced
35905:3d699b736ff4 35906:e0382e4b4da7 
    60   end;
 
    60   end;
 
    61 
    61 
    62 
    62 
    63 (*** Continuous function space ***)
 
    63 (*** Continuous function space ***)
 
    64 
    64 
    65 (* ->> is taken from holcf_logic.ML *)
 
       
    66 fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
 
    65 fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
 
    67 
    66 
    68 val (op ->>) = mk_cfunT;
 
    67 val (op ->>) = mk_cfunT;
 
    69 val (op -->>) = Library.foldr mk_cfunT;
 
    68 val (op -->>) = Library.foldr mk_cfunT;
 
    70 
    69
isabelle