Lines Matching refs:HOL
2 (* Various ML tools to support ACL2 in HOL including: *)
4 (* 1. A printer from HOL to ACL2. *)
8 (* to HOL term. *)
97 (* Error reporting function (uses some HOL boilerplate I don't understand) *)
201 (* 3. Uses the HOL overloading mechanism to introduce "hol_name" *)
203 (* a valid HOL identifier name). *)
282 print "\" defined with HOL name \"";
330 print "\" defined with HOL name \"";
348 (out("; File created from HOL using print_lisp_file on " ^ date() ^ "\n\n");
789 (* a negative integer to HOL representation). *)
939 (* Get the HOL name from ACL2 name. *)
940 (* If there is no HOL name (e.g. an ACL2 variable) the ACL2 name is *)
1162 (* Code for processing ACL2 defuns slurped into HOL via Matt's a2ml tool *)
1197 (* corresponding HOL s-expression (sexp). *)
1216 (* corresponding HOL s-expression (sexp). *)
1234 (* Convert an ML s-expression (mlsexp) to the coresponding HOL *)
1305 (* Look up the HOL name of an ACL2 name and return the corresponding *)
1306 (* term. Return a variable with a supplied type if there is no HOL name. *)
1468 The method of converting a full ACL2 name pkg::sym to a HOL-friendly
1471 1. First see if the ACL2 name already has a HOL name, and if so
1474 2. Convert sym to a HOL name, say hol_sym, using the ML function
1492 HOL-friendly name as follows.
1511 (* Map from ACL2 characters in names to lists of HOL-friendly characters. *)
1533 (* Convert a character to a list of HOL-friendly characters by applying *)
1553 (* ACL2 to HOL name conversion function. Treats first character specially. *)
1561 (* Create a HOL-friendly name from a full ACL2 name and remember it in *)
1564 (* The package name is eliminated unless it's needed to disambiguate HOL *)
1628 (* ML datatype to represent HOL tems and other data (e.g. names) of *)
1673 (* Used for reproving ACL2 imports inside HOL and for round-trip printing. *)
2066 (* 2. declare HOL-friendly names (declare_names) using names generated *)
2069 (* 3. create theorems using mk_oracle_thm then save them with a HOL-friendly *)
2287 out("(* File created from HOL using print_acl2_defun_script on "