*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] New AFP theory: List Index*From*: Makarius <makarius at sketis.net>*Date*: Mon, 22 Feb 2010 13:02:33 +0100 (CET)*In-reply-to*: <cc2478ab1002210706h72b0eb44wa9ed3f35e737fac5@mail.gmail.com>*References*: <4B803BB1.6000907@in.tum.de> <D5B95A2A-767C-40A5-8A97-B2A67A744057@cse.unsw.edu.au> <4B80EA88.8090500@in.tum.de> <4B80F4FC.8020300@uni-muenster.de> <cc2478ab1002210706h72b0eb44wa9ed3f35e737fac5@mail.gmail.com>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Sun, 21 Feb 2010, Brian Huffman wrote:

If users want hierarchical module names, why don't we (the Isabelle developers) just implement that feature? The implementation wouldn't involve much: 1. Make the dot "." a legal character in module names.2. Define a new mapping from module names to filepaths, so that "importsA.B.C" makes Isabelle load the file "~/A/B/C.thy", where "~" is filledin with some directory from the search path.

All of this is completely non-trivial.

Makarius

**References**:**[isabelle] New AFP theory: List Index***From:*Tobias Nipkow

**Re: [isabelle] New AFP theory: List Index***From:*Simon Winwood

**Re: [isabelle] New AFP theory: List Index***From:*Tobias Nipkow

**Re: [isabelle] New AFP theory: List Index***From:*Peter Lammich

**Re: [isabelle] New AFP theory: List Index***From:*Brian Huffman

- Previous by Date: Re: [isabelle] New AFP theory: List Index
- Next by Date: Re: [isabelle] Should isatool document preparation preserve timestamps while copying?
- Previous by Thread: Re: [isabelle] New AFP theory: List Index
- Next by Thread: Re: [isabelle] New AFP theory: List Index
- Cl-isabelle-users February 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list