We probably still have a few occurrences of these, but no problem phasing them
out.
Cheers,
Gerwin
On 09.11.2018, at 10:03, Peter Lammich
mailto:lamm...@in.tum.de>> wrote:
I sometimes see {* *} in old theory files, and find it funny to be reminded
that this was standard only 5 years ago ...
I sometimes see {* *} in old theory files, and find it funny to be reminded that this was standard only 5 years ago ... from my side there are no uses of this quotation remaining that I'd know ofHowever, (* *) is still very important for informally andquickly commenting things out, also in inner
> On 8 Nov 2018, at 20:32, Makarius wrote:
>
> In particular, what are the remaining uses of {* ... *}?
I didn’t even know that existed.
But I use (*...*) to enclose arbitrary text or comment material out.
___
isabelle-dev mailing list
Over the decades we have accumulated funny quotation forms in Isabelle
syntax that are often hard to explain to new users (also to old users).
In particular, what are the remaining uses of {* ... *}?
It should already be superseded by cartouches. There is also "isabelle
update_cartouches" to get
This is the updated situation according to Isabelle/c1a27fce2076:
*** System ***
* Support for managed installations of Glasgow Haskell Compiler and
OCaml via the following command-line tools:
isabelle ghc_setup
isabelle ghc_stack
isabelle ocaml_setup
isabelle ocaml_opam
The global
Makarius wrote:
> On 08/11/2018 14:59, Bertram Felgenhauer wrote:
> >>
> >> I've misunderstood the problem. You intend to invoke old-style
> >> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
> >> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.
> >
On 08/11/2018 14:59, Bertram Felgenhauer wrote:
>>
>> I've misunderstood the problem. You intend to invoke old-style
>> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
>> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.
>
> This may be premature,
Makarius wrote:
> On 08/11/2018 11:30, Bertram Felgenhauer wrote:
> > Makarius wrote:
> >> Nonetheless, it is still possible to use "isabelle ghc" without stack:
> >> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
> >> Isabelle settings mechanism to override ISABELLE_GHC with
On 08/11/2018 12:16, Makarius wrote:
> On 08/11/2018 11:30, Bertram Felgenhauer wrote:
>> Makarius wrote:
>>> Nonetheless, it is still possible to use "isabelle ghc" without stack:
>>> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
>>> Isabelle settings mechanism to override
On 08/11/2018 11:30, Bertram Felgenhauer wrote:
> Makarius wrote:
>> Nonetheless, it is still possible to use "isabelle ghc" without stack:
>> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
>> Isabelle settings mechanism to override ISABELLE_GHC with the
>> stack-based tools.
Makarius wrote:
> Nonetheless, it is still possible to use "isabelle ghc" without stack:
> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
> Isabelle settings mechanism to override ISABELLE_GHC with the
> stack-based tools.
After purging $ISABELLE_STACK_ROOT, `isabelle ghc`
11 matches
Mail list logo
