<!-- $Revision: 0.00.44 $ -->


MODULE(
  HEADER(
    SPEC(
      NAME("")         name of this module, must be identical with    
                        first part of file name
      VERSION("")      modul version, must be identical with last part
                        of file name
      VERSION("")      needs this rule version
      LOCATIONS(
        LOCATION("")   + local or web or relative URL of this module 
                        file
      )
    )
    HEADLINE("")       headline of module
    DESCRIPTION("")    describes contents
    EMAIL("")          email to this address if you want to inform the
                        module administrator (e.g. about referencing
                        this module)
    AUTHORS(
      AUTHOR(          + author of this module
        ""             name of author
        EMAIL("")      *
    )
  )
  IMPORTS(             ?
    IMPORT(            * these external modules are needed
      SPEC(
        NAME("")       name of needed module
        VERSION("")    version of needed module
        VERSION("")    rule version needed module needs
        LOCATIONS(     
          LOCATION("") local or web or relative URL of module
        )
      )
      LABEL("")        ? label to use for that module
                        if missing, all labels of that module are
                        added directly
    )
  )
  USEDBY(              ?
    SPEC(              +
      NAME("")         name of module, must be identical with    
                        first part of file name
      VERSION("")      modul version, must be identical with last part
                        of file name
      VERSION("")      needs this rule version
      LOCATIONS(
        LOCATION("")   + local or web or relative URL of module file
      )
    )
  )
  PARAGRAPHS(
    PARAGRAPH(         * the meat
      LABEL("")        for referenceing
      ""               ? preceeding text
      {ABBREVIATION |
       AXIOM |
       PROPOSITION
      }
      ""               ? following text        
  )
) 

PROPOSITION must be in {REMARK, LEMMA, THEOREM}

DEFINITION(
  NAME("")             ?
  LABEL("")
  EXPORT               ? necessary???
  DEFINITION           like logic.basic defines it
)

Text could include links to labels
In proofs externel references could be made by "alias.label",
internal references are made by "label"

Version numbers are counted as follows:

,- main version, no compatiblity guaranteed
| ,- compatible version, any reference should work further on 
| |   could have more paragraphs
| |   - compatible version (only different comments, or proofs, 
| |  |   no different imports. rule version might be lower
| |  |
0.00.00  normal formatting (could be extended: 0.00001.000001)

The file name is build by the name of the module, followed by 
a "." and the version number of the module and a "_" and the rule 
version number and the extension ".qedeq"


A local url will represent the web location it came from:

http://www.meyling.com/principia/logic/propaxiom_1.00.00_1.00.00.qedeq
 has the following local representation:
principia/buffer/http/www.meyling.com/principia/logic/propaxiom_1.00.00_1.00.00.qedeq

ftp://meyling.com/principia/logic/propaxiom_1.00.00_1.00.00.qedeq
 has the following local representation:
principia/buffer/ftp/www.meyling.com/principia/logic/basic_1.00.00_1.00.00.qedeq

Imports could have relative paths (relative to current module)

Once a module is successfully loaded it makes an entry into an 
global hash table (entry: local url). If there is already an entry
a conflict occures.
If a module is needed (IMPORT), the urls are tried successcive:
first the hash table is searched, then the urls itself.