INT_OF_REAL_THM : thm -> thm
# REAL_ABS_TRIANGLE;; val it : thm = |- !x y. abs (x + y) <= abs x + abs y # map dest_var (variables(concl it));; val it : (string * hol_type) list = [("y", `:real`); ("x", `:real`)] # INT_OF_REAL_THM REAL_ABS_TRIANGLE;; val it : thm = |- !x y. abs (x + y) <= abs x + abs y # map dest_var (variables(concl it));; val it : (string * hol_type) list = [("y", `:int`); ("x", `:int`)]