function ShowProof(lname,b) {
  eval("parent."+lname+" = "+b); location.href="#"+lname; location.reload();location.href="#"+lname;
}

function EndLemma(lname,lnum) {
  if ((navigator.appVersion.indexOf("Safari") < 0) && (eval("parent."+lname) != 1)) {
    document.write('<A HREF=javascript:{ShowProof("'+lname+'","1");}>'+lnum+'</A>');
  }
  else {
    document.write(lnum);
  }
}

function StartProof(lname) {
  if ((navigator.appVersion.indexOf("Safari") < 0) && (eval("parent."+lname) != 1)) {
    document.write('<'+'!--');
  }
}

function EndProof(lname) {
  if (navigator.appVersion.indexOf("Safari") >= 0) {
    document.write('<IMG WIDTH="10" HEIGHT="10" ALIGN="BOTTOM" BORDER="0" SRC="../cube-r.png">');
  }
  else {
    document.write('<A HREF=javascript:{ShowProof("'+lname+'","0");}><IMG WIDTH="10" HEIGHT="10" ALIGN="BOTTOM" BORDER="0" SRC="../cube-r.png"></A>');
  }
}

function LibRef(book,event) {
  w=(screen.width)?(screen.width)/1.5:700;
  h=(screen.height)?(screen.height-150):900;
  if (!parent.codewin || !parent.codewin.open) {
    parent.codewin = parent.window.open('../lib/basic.html','lib','width='+w+',height='+h+',top=100,left=100,scrollbars=yes,'+'location=yes,directories=no,status=no,menubar=no,toolbar=yes,resizable=yes');
  }
  parent.codewin.location = "../lib/"+book+".html#"+event;parent.codewin.focus();
}