One page in Concrete Semantics contains the following output that is a
pretty-printed HOL formula:
step S27
(x ::= Plus (V x) (N 1) {{}};;
x ::= Plus (V x) (N 2) {Q}) =
...
With db9996a84166 it prints like this:
step S27 (x ::= Plus (V x) (N 1) {{}};;
x ::= Plus (V x) (N 2) {Q})
On Sat, 9 Jan 2016, Tobias Nipkow wrote:
One page in Concrete Semantics contains the following output that is a
pretty-printed HOL formula:
step S27
(x ::= Plus (V x) (N 1) {{}};;
x ::= Plus (V x) (N 2) {Q}) =
...
With db9996a84166 it prints like this:
step S27 (x ::= Plus (V x) (N 1)
