Re: [isabelle] [isabelle-dev] Some missing setup for function package in combination with Option-type



On Sun, Feb 19, 2012 at 9:19 PM, Makarius <makarius at sketis.net> wrote:
>> - installing entries (+ dependencies; something like cabal for Haskell)
>
> What means "installing"?  Once we have a proper session specification in the
> source trees (not ROOT.ML nor IsaMakefile) you merely point to such points
> in the file space without "installation".  Or did you mean installation of
> so-called Isabelle components?

I would interpret "installing" to mean downloading theory files and
putting them into an appropriate place in the user's filesystem. After
"installing" an entry or theory library, users should be able to
easily import that library into their own theory files, by writing
something reasonable on the "imports" line (i.e., no absolute or
user-specific path names, but rather something portable that would
work also for anyone else who has installed the same library).

- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.