Hi Chris,
In the Simplifier Trace panel itself I did not find out how to get
any output. Only after pressing the "Show Trace" button a new window
opens that contains the output.
yes, this is working as intended. The panel itself only shows
interactive questions to the user, and by default, th
> Now I also remember why <- is not an abbreviations: for analogy with the
> double arrow: <= is important as \, and not an arrow.
In PROLOG tradition, there is a preference for =< to denote »less or
equal«, to keep <= as double left arrow. But this is maybe too late to
change such a fundamental
Hi all,
As you may know, Sascha and I have been working on a new version of the "smt"
proof method, called "smt2". It is effectively a clone of "smt", but with the
Z3 interaction (problem generation, proof parsing, and reconstruction)
rewritten from scratch, with the following short-term goals:
