Input script: https://cr.yp.to/2023/20230812/step-hol-light-example-1.ml

Definitions have to be copied into HOL Light separately.

Put cursor anywhere in proof and type Ctrl-N ("next"): https://cr.yp.to/2023/20230812/step-hol-light-example-2.ml

Cursor moves after the |# symbol. Goals shown in separate window: https://cr.yp.to/2023/20230812/step-hol-light-example-2-goals.txt

Type Ctrl-N to move to the next step: https://cr.yp.to/2023/20230812/step-hol-light-example-3.ml https://cr.yp.to/2023/20230812/step-hol-light-example-3-goals.txt

Type Ctrl-N to move to the next step: https://cr.yp.to/2023/20230812/step-hol-light-example-4.ml https://cr.yp.to/2023/20230812/step-hol-light-example-4-goals.txt

Type Ctrl-X to execute the entire proof. The |# disappears, and the HOL Light session now knows the proof.

Put cursor at the beginning of the qed line and type Ctrl-H ("here"): https://cr.yp.to/2023/20230812/step-hol-light-example-5.ml https://cr.yp.to/2023/20230812/step-hol-light-example-5-goals.txt

Type Ctrl-P ("previous"): https://cr.yp.to/2023/20230812/step-hol-light-example-6.ml https://cr.yp.to/2023/20230812/step-hol-light-example-6-goals.txt