[Hol-info] hol-online not working

Hi, Does anyone have a link to HOL light online that works? https://code.google.com/archive/p/hol-online/ thanks! - Brando Miranda PhD Student Computer Science at University of Illinois at Urbana-Champaign (UIUC) Alfred P. Sloan Scholar | SURGE Fellow | Saburo Muroga Endowed Fellow

[Hol-info] grammar for HOL Light terms

Hi, This is my first message to the HOL list so hope its not out of the rules for the list (couldn’t find the rules). I wanted to find the formal grammar for generating terms (formulas) in HOL (Light). I was wondering were I could find such a specification? Thanks! Brando