paulch42

The following proof works (only change is in the last few lines): ``` theorem mul_left_cancel (a b c : MyNat) (ha : a ≠ 0) : a * b =...

Another useful enhancement to the LaTeX output would be the ability to select a subset of modules. At present it is only possible to select the project and generate LaTeX,...

As a very simple example of an explorer capability, the attached adds two files. View 'frame.html' in a browser as the starting point. [vdm.zip](https://github.com/overturetool/overture/files/1150165/vdm.zip)

Since we are on the topic of F3. One of the nice things about browsing in HTML is the ease with which you can return to what you were viewing...

I have noticed the same issue. If you look at item 4 in #593 there is the comment: "There is an 'Open Declaration' item which works in some cases." I...