Hi everybody, I am working on the VirtualBox 4.02/Ubuntu 12.04 LTS, windows 10 as guest OS. I installed the HOL Light following the isntruction on link:
https://bitbucket.org/akrauss/hol-light-workbench It uses Ocaml version 3.12.1/camlp5-5.15, a slight modification in the setup script for downloading the Hol Light from git clone https://github.com/jrh13/hol-light.git I use following code fregment for showing types: let print_typed_var fmt tm = let s,ty = dest_var tm in pp_print_string fmt ("("^s^":"^string_of_type ty^")") in install_user_printer("print_typed_var",print_typed_var);; When I upload the "Multivariate/make_complex.ml" or simply some other theory (let us say "Multivariate/topology.ml"), and want to know about the types I come up with datatypes of numerical attributes, e.g, # TENDSTO_REAL;; val it : thm = |- ((s:?1143113->real) ---> (l:real)) = (lift o (s:?1143113->real) --> lift (l:real)) I have emacs23. Thanks in advance ------------------------------------------------------------------------------ Mobile security can be enabling, not merely restricting. Employees who bring their own devices (BYOD) to work are irked by the imposition of MDM restrictions. Mobile Device Manager Plus allows you to control only the apps on BYO-devices by containerizing them, leaving personal data untouched! https://ad.doubleclick.net/ddm/clk/304595813;131938128;j _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
