function mouse_over(name ,dest)
{
    name.src = dest;
}


function show_header_line(element)
{
document.getElementById(element+'_').style.visibility = 'visible';
}


function hide_header_line(element)
{
document.getElementById(element+'_').style.visibility = 'hidden';
}