Re: [Hol-info] How to transform the proof form

For HOL Light I've got a tool called Tactician that would be ideal for that: http://www.proof-technologies.com/tactician/ but it doesn't work for HOL4. One day I hope to port it, but that's unlikely to be done in the near future. Mark. on 27/11/15 8:20 AM, Ada wrote: >

[Hol-info] How to transform the proof form

Hey guys, I am learning to use HOL. Here is some code. load "abs_tools"; open abs_tools; val _ = type_abbrev ("num_field", ``:complex -> bool``); (* --