Hi Makarius,
the same goes for me. Installing and running this worked without any
trouble when following your instructions.
One thing that disturbed me in the beginning was that I first have to edit
a document before any symbols get prettified.
Simon
On Mon, Jul 3, 2017 at 4:11 PM Mathias
Dear Makarius,
I am using Isabelle/VSCode code for a week now. So it is possible to
install and use it.
I mostly like it:
* I really like VSCode's Control-P to search for commands.
* the PIDE protocol, unlike "isabelle build", accepts unicode
characters: If the file contains "×⇩r"
On 30/06/17 16:39, Manuel Eberl wrote:
>
> The advantage of qualified names is that they really allow us to add
> disambiguating context to ambiguous names when necessary, e.g. something
> like "List.subseq" and "Topological_Spaces.subseq". Still, as I said, I
> do understand that typing such
*** General ***
* Commands 'alias' and 'type_alias' introduce aliases for constants and
type constructors, respectively. This allows adhoc changes to name-space
accesses within global or local theory contexts, e.g. within a 'bundle'.
This refers to Isabelle/df85956228c2. These are fully
On 07/02/2017 10:59 PM, Makarius wrote:
> On 02/07/17 22:16, Christian Sternagel wrote:
>>
>>> It should work analogously to the "Preview" button, but without having a
>>> button.
>>
>> Preview (more concretely the "Open Preview" "button" -- some kind of
>> magnifying glass icon where the rest is
See now Isabelle/4c999b5d78e2.
Andreas
On 30/06/17 21:31, Tobias Nipkow wrote:
On 30/06/2017 20:41, Manuel Eberl wrote:
By the way, I recently encountered a similar (and even more nasty)
name clash, with compact. The following works perfectly
It's "Topological_Spaces.compact" and that
Hi all,
Yes, it absolutely makes sense to change the situation with compact. It is a standard
notion in order theory, so my suggestion is to make it qualified with ccpo, just like
admissible and fixp are. I can take care of that.
Andreas
On 30/06/17 21:31, Tobias Nipkow wrote:
On
