1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* HOL LIGHT pervasives *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
11 This module contains things in HOL Light that clash and get overwriten.
12 This file needs to be loaded immediately after
13 tactics.ml and lib.ml to get the intended values.
19 module Hol_pervasives = struct
21 let e tac = refine(by(VALID tac));;
23 let r n = refine(rotate n);;
26 let fvs = sort (<) (map (fst o dest_var) (frees t)) in
28 let errmsg = end_itlist (fun s t -> s^", "^t) fvs in
29 warn true ("Free variables in goal: "^errmsg)
34 let l = !current_goalstack in
35 if length l = 1 then failwith "Can't back up any more" else
36 current_goalstack := tl l;
42 (* HOL Light lib, in general raises Failure _
43 unlike Ocaml List, which raises Not_found. *)