--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/README Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,92 @@
+The Isabelle webpage
+====================
+
+(1) Philosophy
+==============
+
+The webpage sources consists of three differnt layers:
+
+a) the presentation layer
+-------------------------
+
+This is was the user actually sees; the slogan is
+
+ "structural XHTML plus with CSS"
+
+There are three different groups of end-user agents (browsers)
+
+ 1) "practical non-CSS" browsers (lynx, netscape4)
+ These just display plain HTML
+ 2) "more-or-less-w3c-CSS" browsers (KHTML/Konqueror/Safari, Internet Explorer)
+ These are able to display the pages almost as they should be,
+ but perhaps with some minor warts.
+ 3) "almost-w3-CSS" browsers (Mozilla/Firefox/Galeone)
+ These are the "reference implementation" for the layout
+
+b) the project layer
+--------------------
+
+This manages the dependencies between files; the tool of choice
+is
+
+ "make plus shell scripting"
+
+Project settings may be configured using a seperate configuration
+file
+
+c) the preprocessing layer
+--------------------------
+
+This allows to use things like includes, current date and so on:
+
+ "XHTML plus processing instructions"
+
+Note that this is almosz not interwoven with b), to keep it as robust
+and simple as possible.
+
+The layer itself is implemented by a small tool "pypager", written in python.
+
+
+(2) writing your own pages
+==========================
+
+You may add arbitrary files to the dir structure, but adhere to the following:
+* use XHTML, not loose HTML
+* no structural markup; of you need layout effects, use CSS
+* any files ending with .html are considered as HTML files and are implicitly
+ processed by the preprocessing layer
+* for HTML includes, it is most convenient to name them *.include.html
+* whole dirs maybe selected for statically copying them to the target destination
+ by configuring the project layer
+
+
+(3) using the project layer framework
+=====================================
+
+To configure it the first time after checkout, just type
+> make phase=init
+
+Then, you may edit the project configuration file conf/localconf.mak.
+After a correct configuration, the build process may be started by
+> make
+
+The project layer tries to be smart about dependencies, but inlucdes,
+embedded images and so on are not tracked; to built dependencies anew,
+do
+> make depends
+
+After adding or deleting files, an
+> make depends
+may also be neccessary. The same after changing something in the configuration.
+
+If nothing seems to be sensible any more, try
+> make clean
+> make depends
+> make
+
+
+(4) project-specific remarks
+============================
+
+* the site is not monolithic
+* it must fit neatlessly into the Isabelle distribution and regression framework
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/build/img.memo.txt Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,7 @@
+mogrify -interlace line -strip -trim screenshot_isabelle_macos.gif
+convert -interlace line -scale x55 univ_tum_proto.gif univ_tum.gif
+convert -interlace line -scale x55 univ_cambridge_proto.gif univ_cambridge.gif
+convert -interlace line -scale x100 isabelle.gif isabelle_logo.gif
+convert -interlace line -scale '16x16!' isabelle.gif favicon.gif
+convert -interlace line -scale x125 tutorial_cover_big.gif tutorial_cover_small.gif
+convert -interlace line -scale 250x isabelle_pg_screenshot_big.png isabelle_pg_screenshot_small.png
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/build/localconf.at.template.mak Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,33 @@
+# isaweb configuration
+# $Id$
+
+# python interpreter (> 2.2)
+PYTHON=python
+
+# GNU find
+FIND=find
+
+# HTML tidy (needs not to be set if tidy usuage is disabled, see below)
+TIDY=tidy
+
+# dirs to copy to build target
+COPYDIRS=img media dist/css dist/img
+
+# build target (attention: ~ will not work!)
+OUTPUTROOT=$(HOME)/isaweb_public
+
+# current distribution name
+DISTNAME=Isabelle2004
+
+# location of isabelle distribution packages
+ISABELLE_DIST=/home/html/isabelle/html-data/dist
+
+# location of doc content file
+ISABELLE_DOC_CONTENT_FILE=$(HOME)/isabelle/Distribution/doc/Contents
+
+# set to a true value to use the "pypager iso-8859-1" hack
+# (may be neccessary for older versions of HTML tidy)
+FORCE_ISO_8859_1=
+
+# set to a true value to disable html tidy postprocessing
+DISABLE_TIDY=
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/build/localconf.sun.template.mak Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,33 @@
+# isaweb configuration
+# $Id$
+
+# python interpreter (> 2.2)
+PYTHON=python2.3
+
+# GNU find
+FIND=gfind
+
+# HTML tidy (needs not to be set if tidy usuage is disabled, see below)
+TIDY=tidy
+
+# dirs to copy to build target
+COPYDIRS=img media dist/css dist/img
+
+# build target (attention: ~ will not work!)
+OUTPUTROOT=$(HOME)/isaweb_public
+
+# current distribution name
+DISTNAME=Isabelle2004
+
+# location of isabelle distribution packages
+ISABELLE_DIST=/home/html/isabelle/html-data/dist
+
+# location of doc content file
+ISABELLE_DOC_CONTENT_FILE=$(HOME)/isabelle/Distribution/doc/Contents
+
+# set to a true value to use the "pypager iso-8859-1" hack
+# (may be neccessary for older versions of HTML tidy)
+FORCE_ISO_8859_1=
+
+# set to a true value to disable html tidy postprocessing
+DISABLE_TIDY=
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/build/main.mak Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,125 @@
+# isaweb makefile
+# $Id$
+
+# force shell
+SHELL=bash
+
+# some global variables
+CONF=conf/localconf.mak
+
+# configuration switch
+ifeq ($(phase), init)
+
+# allocate configuration
+init:
+ mkdir -p conf
+ case $$HOSTNAME in sunbroy*) ARCH=sun;; *) ARCH=at;; esac; \
+ sed 's/# $$Id.*//g' build/localconf.$$ARCH.template.mak > $(CONF)
+ $$EDITOR $(CONF)
+ @false
+.PHONY: init
+
+else
+
+# default target
+default: site
+
+# check configuration
+include $(CONF)
+$(CONF):
+ @if [ ! -e $(CONF) ]; \
+ then \
+ echo 'Framework not configured yet; set EDITOR environment variable'; \
+ echo 'to your favorite editor and type'; \
+ echo; \
+ echo ' make phase=init'; \
+ echo; \
+ echo 'to configure it'; \
+ false; \
+ else \
+ :; \
+ fi
+
+# tidy handling
+ifeq ($(DISABLE_TIDY),)
+TIDYCMD=$(TIDY) -q -i -asxhtml --output-xhtml true \
+ --doctype auto \
+ --literal-attributes true \
+ --wrap 0 \
+ --indent auto --indent-spaces 2 \
+ --input-encoding utf8 --output-encoding latin1 \
+ --logical-emphasis yes --gnu-emacs yes --write-back yes
+else
+TIDYCMD=:
+endif
+
+# dependencies
+DEP_FILE=conf/depends.mak
+site: $(DEP_FILE) allsite
+.PHONY: site
+
+# import dependencies
+include $(DEP_FILE)
+endif
+
+# pypager iso-8859-1 hack
+ifneq ($(FORCE_ISO_8859_1),)
+FORCE_ENC_CMD=--encodinghtml "iso-8859-1"
+else
+FORCE_ENC_CMD=
+endif
+
+# import project-specific dependencies
+include build/project.mak
+
+# build dependencies
+$(DEP_FILE): $(CONF)
+ rm -f $(DEP_FILE); \
+ touch $(DEP_FILE); \
+ echo '# This is a generated file; do not edit' >> $(DEP_FILE); \
+ echo >> $(DEP_FILE); \
+ allstatic=''; \
+ for dir in $(STATICDIRS); \
+ do \
+ for file in `$(FIND) $$dir -type f -a ! -path "*/CVS/*"`; \
+ do \
+ outputfile=$(OUTPUTROOT)/$$file; \
+ outputdir=`dirname $$outputfile`; \
+ echo "$$outputfile: $$file" >> $(DEP_FILE); \
+ echo " mkdir -p $$outputdir" >> $(DEP_FILE); \
+ echo ' cp $$< $$@' >> $(DEP_FILE); \
+ allstatic="$$allstatic$$outputfile "; \
+ echo >> $(DEP_FILE); \
+ done; \
+ done; \
+ echo "DEP_ALLSTATIC=$$allstatic" >> $(DEP_FILE); \
+ echo >> $(DEP_FILE); \
+ echo 'DEP_HTML=$$(DEP_ALLSTATIC) $$(DEP_SYMLINKS) include/documentationdist.include.html $(DEP_FILE) $(CONF)' >> $(DEP_FILE); \
+ echo >> $(DEP_FILE); \
+ allhtml=''; \
+ for html in `$(FIND) . -name "*.html" -a ! -name "*.include.html"`; \
+ do \
+ outputfile=$(OUTPUTROOT)/$$html; \
+ outputdir=`dirname $$outputfile`; \
+ echo "$$outputfile: $$html"' $$(DEP_HTML)' >> $(DEP_FILE); \
+ echo " mkdir -p $$outputdir" >> $(DEP_FILE); \
+ echo ' $(PYTHON) build/pypager.py --dtd="dtd/" $(FORCE_ENC_CMD) --srcroot="." --dstroot="$(OUTPUTROOT)" distname="$(DISTNAME)" $$< $$@' >> $(DEP_FILE); \
+ echo ' -$(TIDYCMD) $$@' >> $(DEP_FILE); \
+ allhtml="$$allhtml$$outputfile "; \
+ echo >> $(DEP_FILE); \
+ done; \
+ echo "DEP_ALLHTML=$$allhtml" >> $(DEP_FILE); \
+ echo >> $(DEP_FILE); \
+ echo 'allsite: $$(DEP_ALLHTML) $$(DEP_ALLSTATIC)' >> $(DEP_FILE); \
+ echo ".PHONY: allsite" >> $(DEP_FILE)
+
+# build dependencies explicitly
+depends:
+ rm -f $(DEP_FILE)
+ $(MAKE) $(DEP_FILE)
+.PHONY: depends
+
+# clean build files
+clean:
+ rm -f $(DEP_FILE)
+.PHONY: clean
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/build/mkcontents.pl Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,70 @@
+#!/usr/bin/perl
+
+# mkcontents.pl
+#
+# $Id$
+#
+# simple script to create a html version of the Contents file in the
+# Isabelle documentation directory.
+#
+# Nov/14/1999 Version 1.0 - Gerwin Klein <kleing@in.tum.de>
+#
+# command line:
+# mkcontent.pl [-p <url-path-prefix>] <Content-file> <output-file>
+#
+
+
+use Getopt::Long ;
+
+$opt_p="";
+$result = GetOptions ("p=s");
+
+$path=$opt_p;
+
+$infile = $ARGV[0];
+$outfile = $ARGV[1];
+
+$listHeader = "<ul>\n";
+$lineHeader = " <li>";
+$lineEnd = "</li>\n";
+$listFooter = "</ul>\n";
+
+$topicStart = "<h3>";
+$topicEnd = "</h3>\n";
+
+open(IN, "<$infile") || die "cannot read input file <$infile>";
+open(OUT, ">$outfile") || die "cannot write output file <$outfile>";
+
+$first = 1;
+
+print OUT '<?xml version="1.0" encoding="iso-8859-1" ?>' . "\n";
+print OUT '<dummy:wrapper xmlns:dummy="http://nowhere.no">' . "\n";
+
+while (<IN>) {
+ if (/^([^ \t].*)\n/) {
+ if ($first == 1) {
+ $first = 0;
+ }
+ else {
+ print OUT $listFooter;
+ }
+ print OUT $topicStart;
+ print OUT $1;
+ print OUT $topicEnd;
+ print OUT $listHeader;
+ }
+ elsif (/^[ \t]+([^ \t]+)[ \t]+(.+)\n/) {
+ print OUT $lineHeader;
+ print OUT "<a target='_blank' href='$path$1.pdf'>$2</a>";
+ print OUT $lineEnd;
+ }
+}
+
+print OUT $listFooter;
+
+print OUT '</dummy:wrapper>' . "\n";
+
+close(OUT);
+close(IN);
+
+exit(0);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/build/project.mak Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,11 @@
+# isaweb makefile - project-specific dependencies
+# $Id$
+
+DEP_SYMLINKS=$(OUTPUTROOT)/dist/packages
+
+$(DEP_SYMLINKS): $(ISABELLE_DIST)
+ mkdir -p $(OUTPUTROOT)/dist
+ ln -s $< $@
+
+include/documentationdist.include.html: $(ISABELLE_DOC_CONTENT_FILE)
+ perl build/mkcontents.pl -p '//dist/packages/Isabelle/doc/' $< $@
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/build/pypager.py Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,452 @@
+#!/usr/bin/env python
+# -*- coding: Latin-1 -*-
+
+__author__ = 'Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de'
+__revision__ = '$Id$'
+
+# generic imports
+import sys
+import os
+from os import path
+import posixpath
+import codecs
+import shlex
+import optparse
+import time
+
+# xml imports
+from xml.sax.saxutils import escape
+from xml.sax.saxutils import quoteattr
+from xml.sax import make_parser as makeParser
+from xml.sax.handler import ContentHandler
+from xml.sax.handler import EntityResolver
+from xml.sax.xmlreader import AttributesImpl as Attributes
+from xml.sax import SAXException
+from xml.sax import SAXParseException
+
+nbsp = unichr(160)
+
+# global configuration
+outputEncoding = 'UTF-8'
+
+# implement your own functions for PIs here
+class Functions:
+
+ def __init__(self, pc, valdict, modtime, encodingMeta):
+
+ self._pc = pc
+ self._valdict = valdict
+ self._modtime = modtime
+ self._encodingMeta = encodingMeta
+
+ def getPc(self):
+
+ return self._pc
+
+ def value(self, handler, **args):
+
+ value = self._valdict[args[u"key"]]
+ handler.characters(value)
+
+ def title(self, handler, **args):
+
+ handler.characters(handler._title)
+
+ def contentType(self, handler, **args):
+
+ encoding = self._encodingMeta or handler._encoding
+ attr = {
+ u"http-equiv": u"Content-Type",
+ u"content": u"text/html; charset=%s" % encoding
+ }
+ handler.startElement(u"meta", attr)
+ handler.endElement(u"meta")
+
+ def currentDate(self, handler, **args):
+
+ handler.characters(unicode(time.strftime('%Y-%m-%d %H:%M:%S')))
+
+ def modificationDate(self, handler, **args):
+
+ handler.characters(unicode(time.strftime('%Y-%m-%d %H:%M:%S',
+ time.localtime(self._modtime))))
+
+ def relativeRoot(self, handler, **args):
+
+ href = args[u"href"].encode("latin-1")
+ handler.characters(self._pc.relDstPathOf('//'+href))
+
+ def include(self, handler, **args):
+
+ filename = args[u"file"].encode("latin-1")
+ filename = self._pc.absSrcPathOf(filename)
+ self._modtime = max(self._modtime, os.stat(filename).st_mtime)
+ istream = open(filename, "r")
+ parseWithER(istream, handler)
+ istream.close()
+
+ def navitem(self, handler, **args):
+
+ target = args[u"target"].encode("latin-1")
+ target = self._pc.relDstPathOf(target)
+ if self._pc.isSrc(target):
+ wrapTagname = u"strong"
+ else:
+ wrapTagname = u"span"
+ title = args[u"title"]
+ attr = {}
+ handler.startElement(u"li", attr)
+ handler.startElement(wrapTagname, {})
+ handler.startElement(u"a", {
+ u"href": unicode(target, 'latin-1')
+ })
+ handler.characters(title)
+ handler.endElement(u"a")
+ handler.endElement(wrapTagname)
+ handler.endElement(u"li")
+
+ def downloadCells(self, handler, **args):
+
+ target = args[u"target"].encode("latin-1")
+ targetReal = self._pc.absDstPathOf(target)
+ title = args.get(u"title", unicode(posixpath.split(target)[0], 'latin-1'))
+ size = os.stat(targetReal).st_size
+ handler.startElement(u"td", {})
+ handler.startElement(u"a", {
+ u"href": target
+ })
+ handler.characters(title)
+ handler.endElement(u"a")
+ handler.endElement(u"td")
+ handler.startElement(u"td", {})
+ handler.characters(u"%i%sKB" % (size / 1024, unichr(160)))
+ handler.endElement(u"td")
+
+ def cvs(self, handler, **args):
+
+ pass
+
+# a notion of paths
+class PathCalculator:
+
+ def __init__(self, srcLoc, srcRoot, dstRoot):
+
+ self._src = path.normpath(path.abspath(srcLoc))
+ srcPath, srcName = path.split(self._src)
+ self._srcRoot = path.normpath(path.abspath(srcRoot))
+ self._dstRoot = path.normpath(path.abspath(dstRoot))
+ self._relRoot = ""
+ relLocChain = []
+ diffRoot = srcPath
+ while diffRoot != self._srcRoot:
+ self._relRoot = path.join(self._relRoot, os.pardir)
+ diffRoot, chainPiece = path.split(diffRoot)
+ relLocChain.insert(0, chainPiece)
+ self._relRoot = self._relRoot and self._relRoot + '/'
+ self._relLoc = relLocChain and path.join(*relLocChain) or ""
+
+ def isSrc(self, loc):
+
+ return self.absSrcPathOf(loc) == self._src
+
+ def relRootPath(self):
+
+ return self._relRoot
+
+ def absSrcPathOf(self, loc):
+
+ if loc.startswith("//"):
+ return path.normpath(path.abspath(loc[2:]))
+ else:
+ return path.normpath(path.abspath(path.join(self._relLoc, loc)))
+
+ def absDstPathOf(self, loc):
+
+ if loc.startswith("//"):
+ return path.join(self._dstRoot, loc[2:])
+ else:
+ return path.join(self._dstRoot, self._relLoc, loc)
+
+ def relSrcPathOf(self, loc):
+
+ loc = self.absSrcPathOf(loc)
+ loc = self.stripCommonPrefix(loc, self._srcRoot)
+ loc = self.stripCommonPrefix(loc, self._relLoc)
+ return loc
+
+ def relDstPathOf(self, loc):
+
+ loc = self.absDstPathOf(loc)
+ loc = self.stripCommonPrefix(loc, self._dstRoot)
+ loc = self.stripCommonPrefix(loc, self._relLoc)
+ return loc
+
+ def stripCommonPrefix(self, loc, prefix):
+
+ common = self.commonPrefix((loc, prefix))
+ if common:
+ loc = loc[len(common):]
+ if loc and loc[0] == '/':
+ loc = loc[1:]
+ return loc
+
+ def commonPrefix(self, locs):
+
+ common = path.commonprefix(locs)
+ # commonprefix bugs
+ if [ loc for loc in locs if len(loc) != common ] and \
+ [ loc for loc in locs if len(common) < len(loc) and loc[len(common)] != path.sep ]:
+ common = path.split(common)[0]
+ if common and common[-1] == path.sep:
+ common = common[:-1]
+
+ return common or ""
+
+# the XML transformer
+class TransformerHandler(ContentHandler, EntityResolver):
+
+ def __init__(self, out, encoding, dtd, func):
+
+ ContentHandler.__init__(self)
+ #~ EntityResolver.__init__(self)
+ self._out = codecs.getwriter(encoding)(out)
+ self._ns_contexts = [{}] # contains uri -> prefix dicts
+ self._current_context = self._ns_contexts[-1]
+ self._undeclared_ns_maps = []
+ self._encoding = encoding
+ self._lastStart = False
+ self._func = func
+ self._characterBuffer = {}
+ self._currentXPath = []
+ self._title = None
+ self._init = False
+ self._dtd = dtd
+
+ def closeLastStart(self):
+
+ if self._lastStart:
+ self._out.write(u'>')
+ self._lastStart = False
+
+ def flushCharacterBuffer(self):
+
+ self._out.write(escape(u"".join(self._characterBuffer)))
+ self._characterBuffer = []
+
+ def transformAbsPath(self, attrs, attrname):
+
+ pathval = attrs.get(attrname, None)
+ if pathval and pathval.startswith(u"//"):
+ attrs = dict(attrs)
+ pathRel = self._func.getPc().relDstPathOf(pathval)
+ pathDst = self._func.getPc().absDstPathOf(pathval)
+ if not path.exists(pathDst):
+ raise Exception("Path does not exist: %s" % pathDst)
+ attrs[attrname] = pathRel
+ return attrs
+ else:
+ return attrs
+
+ def startDocument(self):
+
+ if not self._init:
+ if self._encoding.upper() != 'UTF-8':
+ self._out.write(u'<?xml version="1.0" encoding="%s"?>\n' %
+ self._encoding)
+ else:
+ self._out.write(u'<?xml version="1.0"?>\n')
+ self._init = True
+
+ def startPrefixMapping(self, prefix, uri):
+
+ self._ns_contexts.append(self._current_context.copy())
+ self._current_context[uri] = prefix
+ self._undeclared_ns_maps.append((prefix, uri))
+
+ def endPrefixMapping(self, prefix):
+
+ self._current_context = self._ns_contexts[-1]
+ del self._ns_contexts[-1]
+
+ def startElement(self, name, attrs):
+
+ if name == u"dummy:wrapper":
+ return
+ self.closeLastStart()
+ self.flushCharacterBuffer()
+ self._out.write(u'<' + name)
+ # this list is not exhaustive
+ for tagname, attrname in ((u"a", u"href"), (u"img", u"src"), (u"link", u"href")):
+ if name == tagname:
+ attrs = self.transformAbsPath(attrs, attrname)
+ for (name, value) in attrs.items():
+ self._out.write(u' %s=%s' % (name, quoteattr(value)))
+ self._currentXPath.append(name)
+ self._lastStart = True
+
+ def endElement(self, name):
+
+ if name == u"dummy:wrapper":
+ return
+ elif name == u'title':
+ self._title = u"".join(self._characterBuffer)
+ self.flushCharacterBuffer()
+ if self._lastStart:
+ self._out.write(u'/>')
+ self._lastStart = False
+ else:
+ self._out.write('</%s>' % name)
+ self._currentXPath.pop()
+
+ def startElementNS(self, name, qname, attrs):
+
+ self.closeLastStart()
+ self.flushCharacterBuffer()
+ if name[0] is None:
+ # if the name was not namespace-scoped, use the unqualified part
+ name = name[1]
+ else:
+ # else try to restore the original prefix from the namespace
+ name = self._current_context[name[0]] + u":" + name[1]
+ self._out.write(u'<' + name)
+
+ for pair in self._undeclared_ns_maps:
+ self._out.write(u' xmlns:%s="%s"' % pair)
+ self._undeclared_ns_maps = []
+
+ for (name, value) in attrs.items():
+ name = self._current_context[name[0]] + ":" + name[1]
+ self._out.write(' %s=%s' % (name, quoteattr(value)))
+ self._out.write('>')
+ self._currentXPath.append(name)
+
+ def endElementNS(self, name, qname):
+
+ self.flushCharacterBuffer()
+ if name[0] is None:
+ name = name[1]
+ else:
+ name = self._current_context[name[0]] + u":" + name[1]
+ if self._lastStart:
+ self._out.write(u'/>')
+ self._lastStart = False
+ else:
+ self._out.write(u'</%s>' % name)
+ self._currentXPath.pop()
+
+ def characters(self, content):
+
+ self.closeLastStart()
+ self._characterBuffer.append(content)
+
+ def ignorableWhitespace(self, content):
+
+ self.closeLastStart()
+ self.flushCharacterBuffer()
+ self._out.write(content)
+
+ def resolveEntity(self, publicId, systemId):
+
+ loc, name = posixpath.split(systemId)
+ if loc == u"http://www.w3.org/TR/xhtml1/DTD" or loc == u"":
+ systemId = path.join(self._dtd, name)
+ return EntityResolver.resolveEntity(self, publicId, systemId)
+
+ def processingInstruction(self, target, data):
+
+ self.closeLastStart()
+ self.flushCharacterBuffer()
+ func = getattr(self._func, target)
+ args = {}
+ for keyval in shlex.split(data.encode("utf-8")):
+ key, val = keyval.split("=", 1)
+ args[key] = val
+ func(self, **args)
+
+def parseWithER(istream, handler):
+
+ parser = makeParser()
+ parser.setContentHandler(handler)
+ parser.setEntityResolver(handler)
+ parser.parse(istream)
+
+def main():
+
+ # parse command line
+ cmdlineparser = optparse.OptionParser(
+ usage = '%prog [options] [key=value]* src [dst]',
+ conflict_handler = "error",
+ description = '''Leightweight HTML page generation tool''',
+ add_help_option = True,
+ )
+ cmdlineparser.add_option("-s", "--srcroot",
+ action="store", dest="srcroot",
+ type="string", default=".",
+ help="source tree root", metavar='location')
+ cmdlineparser.add_option("-d", "--dstroot",
+ action="store", dest="dstroot",
+ type="string", default=".",
+ help="destination tree root", metavar='location')
+ cmdlineparser.add_option("-t", "--dtd",
+ action="store", dest="dtd",
+ type="string", default=".",
+ help="local mirror of XHTML DTDs", metavar='location')
+ cmdlineparser.add_option("-m", "--encodinghtml",
+ action="store", dest="encodinghtml",
+ type="string", default="",
+ help="force value of html content encoding meta ", metavar='encoding')
+
+
+ options, args = cmdlineparser.parse_args(sys.argv[1:])
+
+ # check source
+ if len(args) < 1:
+ cmdlineparser.error("Exactly one soure file must be given")
+
+ # read arguments
+ valdict = {}
+ if len(args) == 1:
+ src = args[0]
+ dst = None
+ else:
+ if "=" in args[-2]:
+ src = args[-1]
+ dst = None
+ vallist = args[:-1]
+ else:
+ src = args[-2]
+ dst = args[-1]
+ if dst == "-":
+ dst = None
+ vallist = args[:-2]
+ for keyval in vallist:
+ key, val = keyval.split("=", 1)
+ valdict[unicode(key, 'latin-1')] = unicode(val, 'latin-1')
+
+ # path calculator
+ pc = PathCalculator(src, options.srcroot, options.dstroot)
+
+ # function space
+ modtime = os.stat(src).st_mtime
+ func = Functions(pc, valdict, modtime, options.encodinghtml)
+
+ # allocate file handles
+ istream = open(src, 'r')
+ if dst is not None:
+ ostream = open(dst, 'wb')
+ else:
+ ostream = sys.stdout
+
+ # process file
+ transformer = TransformerHandler(ostream, outputEncoding, options.dtd, func)
+ parseWithER(istream, transformer)
+
+ # close handles
+ ostream.close()
+ istream.close()
+
+if __name__ == '__main__':
+ main()
+
+__todo__ = '''
+'''
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/community.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,52 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Community</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="main">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation.include.html"?>
+ <div class="hr"><hr/></div>
+ <div id="content">
+
+ <h2>Mailing list</h2>
+ <p>
+ You may use the mailing list <a
+ href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
+ and its <a
+ href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to
+ discuss problems and results. To subscribe, <a
+ href="mailto:lcp@cl.cam.ac.uk?subject=subscribe&body=Please%20add%20me%20to%20the%20Isabelle%20mailing%20list">contact
+ Larry Paulson</a>.</p>
+
+ <h2>Contributing theorems</h2>
+
+ <p>Did you have to prove a lemma that should have been part
+ of the Isabelle distribution? Send it to us!</p>
+
+ <p>We will collect theorems sent to <a href=
+ "mailto:isabelle-lemmas@cl.cam.ac.uk">isabelle-lemmas@cl.cam.ac.uk</a>.
+ Accepted material will be included in the Isabelle sources, with credit given
+ to the author. Note that the Isabelle sources are distributed under the BSD
+ license. Lemmas should be general, useful, and not too large. For larger
+ developments you might want to consider a submission to the
+ <a href="http://afp.sf.net">Archive of Formal Proofs</a>.</p>
+
+ <h2 id="afp">The Archive of Formal Proofs (AFP)</h2>
+ <p>The <a href="http://afp.sf.net">Archive of Formal Proofs</a> is a collection of proof
+ libraries, examples, and larger scientifc developments, mechanically checked
+ in Isabelle. It is organized in the way of a scientific journal. Submissions
+ are refereed.</p>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="//include/footer.include.html"?>
+</body>
+
+</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dist/css/aelfwine.css Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,725 @@
+/************************************************************
+ * Stylesheet AElfwine *
+ ************************************************************
+ * *
+ * This has been collected from various sources. *
+ * *
+ * Version 1.0 - 2005/05/01 - f.h. *
+ * *
+ * ...aiming for perfection ;-) *
+ * *
+ ************************************************************/
+
+@namespace url(http://www.w3.org/1999/xhtml); /* DOES ANYONE KNOW WHAT'S THAT ABOUT!? */
+
+/* base paragraph and heading types */
+h1 {
+ display: block;
+
+ font-family: Arial,Helvetica,Verdana,sans-serif;
+ font-style: normal;
+ font-variant: normal;
+ font-size: 2.20em;
+ font-weight: bold;
+ font-stretch: normal;
+ text-decoration: none;
+ text-transform: none;
+ color: #000000;
+ text-shadow: none;
+
+ text-indent: 0.00px;
+ text-align: center;
+ white-space: normal;
+
+ margin-top: 0.62em;
+ margin-bottom: 0.31em;
+ margin-left: 0.00px;
+ margin-right: 0.00px;
+}
+
+h2 {
+ display: block;
+
+ font-family: Arial,Helvetica,Verdana,sans-serif;
+ font-style: normal;
+ font-variant: normal;
+ font-size: 1.77em;
+ font-weight: bold;
+ font-stretch: normal;
+ text-decoration: none;
+ text-transform: none;
+ color: #000000;
+ text-shadow: none;
+
+ text-indent: 0.00px;
+ text-align: center;
+ white-space: normal;
+
+ margin-top: 0.40em;
+ margin-bottom: 0.20em;
+ margin-left: 0.00px;
+ margin-right: 0.00px;
+}
+
+h3 {
+ display: block;
+
+ font-family: Arial,Helvetica,Verdana,sans-serif;
+ font-style: normal;
+ font-variant: normal;
+ font-size: 1.57em;
+ font-weight: bold;
+ font-stretch: normal;
+ text-decoration: none;
+ text-transform: none;
+ color: #000000;
+ text-shadow: none;
+
+ text-indent: 0.00px;
+ text-align: left;
+ white-space: normal;
+
+ margin-top: 0.32em;
+ margin-bottom: 0.10em;
+ margin-left: 0.00px;
+ margin-right: 0.00px;
+}
+
+h4 {
+ display: block;
+
+ font-family: Arial,Helvetica,Verdana,sans-serif;
+ font-style: normal;
+ font-variant: normal;
+ font-size: 1.47em;
+ font-weight: bold;
+ font-stretch: normal;
+ text-decoration: none;
+ text-transform: none;
+ color: #000000;
+ text-shadow: none;
+
+ text-indent: 0.00px;
+ text-align: left;
+ white-space: normal;
+
+ margin-top: 0.29em;
+ margin-bottom: 0.05em;
+ margin-left: 0.00px;
+ margin-right: 0.00px;
+}
+
+h5 {
+ display: block;
+
+ font-family: Arial,Helvetica,Verdana,sans-serif;
+ font-style: normal;
+ font-variant: normal;
+ font-size: 1.18em;
+ font-weight: bold;
+ font-stretch: normal;
+ text-decoration: none;
+ text-transform: none;
+ color: #000000;
+ text-shadow: none;
+
+ text-indent: 0.00px;
+ text-align: left;
+ white-space: normal;
+
+ margin-top: 0.27em;
+ margin-bottom: 0.03em;
+ margin-left: 0.00px;
+ margin-right: 0.00px;
+}
+
+h6 {
+ display: block;
+
+ font-family: Arial,Helvetica,Verdana,sans-serif;
+ font-style: normal;
+ font-variant: normal;
+ font-size: 1em;
+ font-weight: bold;
+ font-stretch: normal;
+ text-decoration: none;
+ text-transform: none;
+ color: #000000;
+ text-shadow: none;
+
+ text-indent: 0.00px;
+ text-align: left;
+ white-space: normal;
+
+ margin-top: 0.25em;
+ margin-bottom: 0.00em;
+ margin-left: 0.00px;
+ margin-right: 0.00px;
+}
+
+p, body, th, td {
+ display: block;
+
+ font-family: Arial,Helvetica,Verdana,sans-serif;
+ font-style: normal;
+ font-variant: normal;
+ font-size: 1.00em;
+ font-weight: normal;
+ font-stretch: normal;
+ text-decoration: none;
+ text-transform: none;
+ color: #000000;
+ text-shadow: none;
+
+ text-indent: 0.00px;
+ white-space: normal;
+
+}
+
+p {
+ text-align: justify;
+ margin-top: 0.20em;
+ margin-bottom: 0.20em;
+}
+
+/* text markup */
+
+em {
+ font-style: italic;
+}
+
+strong {
+ font-weight: bold;
+}
+
+del {
+ text-decoration: line-through;
+}
+
+ins {
+ text-decoration: underline;
+}
+
+/* text format */
+
+sub {
+ vertical-align: sub;
+ font-size: smaller;
+ line-height: normal;
+}
+
+sup {
+ vertical-align: super;
+ font-size: smaller;
+ line-height: normal;
+}
+
+big {
+ font-size: larger;
+}
+
+small {
+ font-size: smaller;
+}
+
+tt {
+ font-family: Courier New,monospace;
+}
+
+pre {
+ display: block;
+ font-family: Courier New,monospace;
+ white-space: pre;
+ margin: 1em 1em;
+}
+
+/* ruler */
+
+hr {
+ display: block;
+ margin: 0 auto 0 auto;
+}
+
+/* document */
+
+html {
+ display: block;
+}
+
+body {
+ display: block;
+ /* KHTML background: #FFFFEE; */
+ margin: 8px;
+}
+
+/* blocks */
+
+div {
+ display: block;
+}
+
+address {
+ display: block;
+ font-style: italic;
+}
+
+blockquote {
+ display: block;
+ margin: 1em 40px;
+}
+
+blockquote[type=cite] {
+ display: block;
+ margin: 1em 0em;
+ padding-left: 1em;
+ border-left: solid;
+ border-color: blue;
+ border-width: thin;
+}
+
+/* spans */
+
+span {
+ display: inline;
+}
+
+abbr, acronym {
+ display: inline;
+}
+
+cite, q {
+ display: inline;
+ font-style: italic;
+}
+
+code, var, kbd {
+ font-family: Courier New,monospace;
+ display: inline;
+}
+
+dfn {
+ display: inline;
+ font-style: italic;
+ font-weight: bold;
+}
+
+samp {
+ display: inline;
+}
+
+/* tables */
+
+table {
+ display: table;
+ margin: 0px;
+ padding: 0px;
+ border-spacing: 1px;
+ border-collapse: separate;
+}
+
+table[align="left"] {
+ float: left;
+}
+
+table[align="right"] {
+ float: right;
+}
+
+caption {
+ display: table-caption;
+}
+
+colgroup {
+ display: table-column-group;
+}
+
+col {
+ display: table-column;
+}
+
+thead {
+ display: table-header-group;
+ vertical-align: middle;
+}
+
+tbody {
+ display: table-row-group;
+}
+
+tfoot {
+ display: table-footer-group;
+ vertical-align: middle;
+}
+
+tr {
+ display: table-row;
+}
+
+th {
+ display: table-cell;
+ font-weight: bold;
+ padding: 1px;
+}
+
+td {
+ display: table-cell;
+ padding: 1px;
+}
+
+/* lists */
+
+ul {
+ display: block;
+ list-style-type: disc;
+ margin: 1em 0em;
+ padding-left: 40px;
+}
+
+ol {
+ display: block;
+ list-style-type: decimal;
+ margin: 1em 0em;
+ padding-left: 40px;
+}
+
+dl {
+ display: block;
+ margin: 1em 0em;
+}
+
+dt {
+ display: block;
+ margin-left: 1em;
+}
+
+dd {
+ display: block;
+ margin-left: 3em;
+}
+
+li {
+ display: list-item;
+}
+
+/* nested lists have no top/bottom margins */
+ul ul, ul ol, ul dl,
+ol ul, ol ol, ol dl,
+dl ul, dl ol, dl dl {
+ margin-top: 0;
+ margin-bottom: 0;
+}
+
+/* 2 deep unordered lists use a circle */
+ol ul, ul ul {
+ list-style-type: circle;
+}
+
+/* 3 deep (or more) unordered lists use a square */
+ol ol ul, ol ul ul,
+ul ol ul, ul ul ul {
+ list-style-type: square;
+}
+
+/* hyperlinks */
+
+a:link {
+ color: #FF0000;
+}
+
+a:visited {
+ color: #FF6600;
+}
+
+a:hover {
+ color: #FF0000;
+}
+
+a:active {
+ color: #FF0000;
+}
+
+a:focus {
+ color: #FF0000;
+}
+
+a[name]:link, a[id]:link:not([href]) {
+ color: #000000;
+}
+
+a[name]:hover, a[id]:hover:not([href]) {
+ color: #000000;
+}
+
+a[name]:active, a[id]:active:not([href]) {
+ color: #000000;
+}
+
+a[name]:focus, a[id]:focus:not([href]) {
+ color: #000000;
+}
+
+a img {
+ border: none;
+}
+
+/* hidden elements */
+area, base, basefont, head, meta, script, style, title,
+noembed, noframes, noscript, param {
+ display: none;
+}
+
+/* forms */
+
+/* misc */
+legend {
+ padding-left: 2px;
+ padding-right: 2px;
+ border: none;
+}
+
+fieldset {
+ display: block;
+ margin-left: 2px;
+ margin-right: 2px;
+ padding: 0.75em 0.625em;
+ border: 2px groove ThreeDFace;
+}
+
+label {
+ cursor: default;
+}
+
+/* default inputs, text inputs, and selects */
+input [type=""], input[type="text"], input[type="password"] {
+ padding: 1px 0px 1px 0px;
+ border: 2px inset ThreeDFace;
+ text-transform: none;
+ vertical-align: text-bottom;
+ cursor: text;
+}
+
+textarea {
+ margin: 1px 0px 1px 0px;
+ border: 2px inset ThreeDFace;
+ font-size: medium;
+ text-transform: none;
+ vertical-align: text-bottom;
+ cursor: text;
+}
+
+select {
+ margin: 0;
+ border-color: ThreeDFace;
+ white-space: nowrap;
+ vertical-align: text-bottom;
+ cursor: default;
+ border-width: 2px;
+ border-style: inset;
+}
+
+select[size] {
+ padding: 1px 0px 1px 0px;
+}
+
+select[size="1"] {
+ padding: 0px;
+}
+
+option {
+ display: block;
+}
+
+option :checked {
+ background-color: Highlight;
+ color: HighlightText;
+}
+
+optgroup {
+ display: block;
+ font-style: italic;
+ font-weight: bold;
+}
+
+optgroup > option {
+ padding-left: 20px;
+ font-style: normal;
+ font-weight: normal;
+}
+
+optgroup :before {
+ display: block;
+ content: attr(label);
+}
+
+option[disabled],
+optgroup[disabled] {
+ background-color: transparent;
+}
+
+/* hidden inputs */
+input[type="hidden"] {
+ display: none;
+ padding: 0em;
+ border: 0em;
+ cursor: auto;
+}
+
+/* image buttons */
+input[type="image"] {
+ padding: 0em;
+ border: none;
+ background-color: transparent;
+ vertical-align: baseline;
+ font-family: sans-serif;
+ font-size: small;
+ cursor: pointer;
+}
+
+input[type="image"][disabled] {
+ cursor: default;
+}
+
+/* file selector */
+input[type="file"] {
+ white-space: nowrap;
+ cursor: default;
+ padding: 0px;
+ border-style: none;
+}
+
+/* radio buttons and check boxes*/
+input[type="radio"] {
+ width: 13px;
+ height: 13px;
+ margin: 3px 3px 0px 5px;
+ padding: 0px;
+ vertical-align: baseline;
+ cursor: default;
+}
+
+/* check boxes */
+input[type="checkbox"] {
+ width: 13px;
+ height: 13px;
+ margin: 3px 3px 3px 4px;
+ padding: 0px;
+ vertical-align: text-bottom;
+ cursor: default;
+}
+
+input[type="checkbox"]:focus,
+input[type="radio"]:focus {
+ border-style: groove;
+}
+
+input[type="checkbox"]:hover:active,
+input[type="radio"]:hover:active {
+ background-color: ThreeDFace;
+ border-style: inset;
+}
+
+/* buttons */
+button,
+input[type="reset"],
+input[type="button"],
+input[type="submit"] {
+ text-transform: none;
+ padding: 2px 0 2px 0;
+ border: 2px outset ButtonFace;
+ background-color: ButtonFace;
+ color: ButtonText;
+ white-space: pre;
+ vertical-align: text-bottom;
+ cursor: default;
+}
+
+button:active:hover,
+input[type="reset"]:active:hover,
+input[type="button"]:active:hover,
+input[type="submit"]:active:hover {
+ padding: 3px 0 1px 0;
+ border-style: inset;
+}
+
+/* disables inputs */
+
+input[disabled],
+textarea[disabled],
+option[disabled],
+optgroup[disabled],
+select[disabled] {
+ color: GrayText;
+ background-color: ThreeDFace;
+ cursor: default;
+}
+
+input[type="radio"][disabled],
+input[type="radio"][disabled]:active,
+input[type="radio"][disabled]:hover,
+input[type="radio"][disabled]:hover:active,
+input[type="checkbox"][disabled],
+input[type="checkbox"][disabled]:active,
+input[type="checkbox"][disabled]:hover,
+input[type="checkbox"][disabled]:hover:active {
+ padding: 1px;
+ border: 1px inset ThreeDShadow;
+ color: GrayText;
+ background-color: ThreeDFace;
+}
+
+button[disabled]:active, button[disabled],
+input[type="reset"][disabled]:active,
+input[type="reset"][disabled],
+input[type="button"][disabled]:active,
+input[type="button"][disabled],
+select[disabled] > input[type="button"],
+select[disabled] > input[type="button"]:active,
+input[type="submit"][disabled]:active,
+input[type="submit"][disabled] {
+ padding: 3px 1px 3px 1px;
+ border: 1px outset ButtonShadow;
+ color: GrayText;
+}
+
+/* DocBook-XSLT-specific extensions */
+
+div.figure {
+ margin-top: 1.9ex;
+}
+
+div.note {
+ margin-top: 1.0ex;
+ margin-bottom: 1.0ex;
+}
+
+div.tip {
+ margin-top: 1.0ex;
+ margin-bottom: 1.0ex;
+}
+
+div.warning {
+ margin-top: 1.0ex;
+ margin-bottom: 1.0ex;
+}
+
+div.caution {
+ margin-top: 1.0ex;
+ margin-bottom: 1.0ex;
+}
+
+div.important {
+ margin-top: 1.0ex;
+ margin-bottom: 1.0ex;
+}
+
+div.figure {
+ margin-bottom: 0.8ex;
+}
+
+div.example {
+ margin-bottom: 0.8ex;
+}
+
+div.equation {
+ margin-bottom: 0.8ex;
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dist/css/isabelle_base.css Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,185 @@
+/************************************************************
+ * Stylesheet Isabelle (all-media basics) *
+ ************************************************************/
+
+/* $Id$ */
+
+@namespace url(http://www.w3.org/1999/xhtml); /* DOES ANYONE KNOW WHAT'S THAT ABOUT!? */
+
+/* generic color settings */
+body {
+ background-color: #FFFFFF;
+}
+
+a:link {
+ color: #0000A0;
+}
+
+a:visited {
+ color: #5050A0;
+}
+
+a:hover {
+ color: #FFFFFF;
+ background-color: #0000FF;
+}
+
+a:hover img {
+ /* gets rid of some of hover highlight */
+ background-color: #FFFFFF;
+}
+
+a:active {
+ color: #00DDFF;
+}
+
+a:focus {
+ color: #00DDFF;
+}
+
+img {
+ border: none;
+}
+
+/* generic formatting */
+h1 {
+ margin-top: 2em;
+ font-size: 230%;
+}
+
+h2 {
+ margin-top: 1em;
+ font-size: x-large;
+ text-align: left;
+ background-color: #8080F0;
+}
+
+h3 {
+ margin-top: 0.7em;
+ font-size: medium;
+ text-align: left;
+ background-color: #8080F0;
+}
+
+p {
+ margin-top: 0.3em;
+ margin-bottom: 0.4em;
+}
+
+/* indendation of following paragraphs */
+/* p + p {
+ text-indent: 0.8em;
+} */
+
+/* navigation layout */
+div#navigation ul {
+ list-style-type: none;
+ margin: 0em;
+ padding: 0em;
+ width: 100%;
+}
+
+/* div#navigation ul li {
+ margin: 5px 0em;
+ padding: 1em 0.5em;
+ text-align: center;
+}
+
+-- perhaps this must be reactivated if the span/strong hack
+ makes problems on non-mozilla browsers
+
+div#navigation ul li.nav_current {
+ background-color: #AAFFAA;
+} */
+
+div#navigation ul li {
+ margin: 0em;
+ padding: 0em;
+}
+
+div#navigation ul li span {
+ display: block;
+ margin: 1ex 0em;
+ padding: 1ex 0em;
+ text-align: center;
+ vertical-align: middle;
+ background-color: #E0E0F0;
+ border-left: 7px solid #FFFFFF;
+}
+
+div#navigation ul li strong {
+ display: block;
+ font-weight: normal;
+ margin: 1ex 0em;
+ padding: 1ex 0em;
+ text-align: center;
+ vertical-align: middle;
+ background-color: #E0E0F0;
+ border-left: 7px solid #0000A0;
+}
+
+body.dist div#navigation ul li strong {
+ border-left: 7px solid #00A000;
+}
+
+/* footer layout */
+div#footer p {
+ text-align: right;
+ font-size: x-small;
+}
+
+/* embedded images */
+img.left {
+ margin-right: 8pt;
+ float: left;
+}
+
+/* shell commands */
+ul.shellcmd {
+ background-color: #8080F0;
+}
+
+ul.shellcmd li:before {
+ content: "> ";
+ font-weight: bold; /* oder gleich grafik */
+}
+
+/* the faq */
+dl.faq dt {
+ background-color: #8080F0;
+ padding: 3px;
+ margin-top: 12px;
+ font-weight: bold;
+}
+
+dl.faq dd {
+ padding: 3px;
+ margin-top: 3px;
+}
+
+/* download tables */
+table.download {
+ margin-top: 2ex;
+ margin-left: auto;
+ margin-right: auto;
+ text-align: center;
+ border-spacing: 4px;
+}
+
+table.download tr td {
+ text-align: left;
+ background-color: #C0C0E0;
+ padding: 0.4ex 1em 0.4ex 1em;
+}
+
+table.download tr td.downloadheader {
+ text-align: left;
+ font-weight: bold;
+ background-color: #8080F0;
+ /* margin-top doesn't seem to work */
+ border-top: 1ex solid #E0E0F0;
+}
+
+table.download tr td + td + td {
+ text-align: right;
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dist/css/isabelle_print.css Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,69 @@
+/************************************************************
+ * Stylesheet Isabelle (print media) *
+ ************************************************************/
+
+/* $Id$ */
+
+@namespace url(http://www.w3.org/1999/xhtml); /* DOES ANYONE KNOW WHAT'S THAT ABOUT!? */
+
+/* use times font for floating text */
+p, body, th, td {
+ font-family: Times New Roman,times,serif;
+}
+
+/* body margin */
+body {
+ margin: 4pt;
+}
+
+/* no rulers (they are just a supplemental for non-css browsers) */
+hr {
+ display: none;
+ visibility: hidden;
+ height: 0pt;
+ width: 0pt;
+}
+
+/* header layout */
+div#header {
+ position: relative;
+ height: 94px;
+ background-color: #FFFFFF;
+}
+
+div#header h1 {
+ position: absolute;
+ top: 0px;
+ left: 0px;
+ margin: 0px;
+}
+
+div#header a#isabelle_logo {
+ position: absolute;
+ right: 0px;
+}
+
+div#header a#univ_tum {
+ display: none;
+}
+
+div#header a#univ_cambridge {
+ display: none;
+}
+
+div#header span.headersep {
+ display: none;
+}
+
+/* navigation layout */
+div#navigation {
+ display: none;
+}
+
+/* footer layout */
+div#footer {
+ position: relative;
+ top: 8px;
+ clear: both;
+ border-top: 2px solid #000000;
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dist/css/isabelle_screen.css Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,113 @@
+/************************************************************
+ * Stylesheet Isabelle (screen media) *
+ ************************************************************/
+
+/* $Id$ */
+
+@namespace url(http://www.w3.org/1999/xhtml); /* DOES ANYONE KNOW WHAT'S THAT ABOUT!? */
+
+/* no rulers (they are just a supplemental for non-css browsers) */
+hr {
+ display: none;
+ visibility: hidden;
+ height: 0pt;
+ width: 0pt;
+}
+
+div.hr {
+ /* a special for KHTML */
+ display: none;
+}
+
+/* header layout */
+div#header {
+ position: relative;
+ height: 90pt;
+ background-color: #FFFFFF;
+}
+
+div#header h1 {
+ /* center between logos */
+ position: absolute;
+ top: 27px;
+ left: 200px;
+ right: 270px;
+ margin: 0px;
+}
+
+div#header a#isabelle_logo {
+ position: absolute;
+ top: 10px;
+ left: 3.2ex;
+}
+
+div#header a#univ_tum {
+ position: absolute;
+ top: 25px;
+ right: 40px;
+}
+
+div#header a#univ_cambridge {
+ position: absolute;
+ top: 25px;
+ right: 130px;
+}
+
+div#header span.headersep {
+ display: none;
+}
+
+/* navigation layout */
+div#navigation {
+ position: relative;
+ top: 2em;
+ left: 1ex;
+ bottom: 4px;
+ padding: 0.5em 0.5em;
+ float: left;
+ width: 15ex;
+ background-color: #FFFFFF;
+ border-top: 2px solid #0000A0;
+ border-bottom: 2px solid #0000A0;
+}
+
+div#navigation h2 {
+ display: none;
+}
+
+/* footer layout */
+div#footer {
+ margin-top: 2em;
+}
+
+/* content layout */
+div#content {
+ position: static;
+ left: 4px;
+ margin-left: 23ex;
+ margin-right: 3%;
+ background-color: #E0E0F0;
+ padding-left: 20px;
+ padding-right: 20px;
+ padding-bottom: 20px;
+}
+
+div#content h2 {
+ margin-left: -20px;
+ margin-right: -20px;
+ padding-left: 20px;
+ padding-top: 0.2ex;
+ padding-bottom: 0.2ex;
+ border-bottom: 1ex solid #E0E0F0;
+}
+
+div#content h3 {
+ margin-right: -20px;
+ padding-top: 0.4ex;
+ padding-bottom: 0.2ex;
+ padding-left: 10px;
+}
+
+body.dist div#content {
+ /* not needed now */
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dist/documentation.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,72 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Documentation</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="dist">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation_dist.include.html"?>
+ <div class="hr"><hr/></div>
+
+ <div id="content">
+
+ <h2>Getting started</h2>
+
+ <a href="//dist/img/tutorial_cover_big.gif">
+ <img class="left" src="//dist/img/tutorial_cover_small.gif" alt="Cover "
+ width="83" height="125"/>
+ </a>
+ <p>For getting started with Isabelle quickly, we recommend the <a href=
+ "//dist/packages/Isabelle/doc/tutorial.pdf">Tutorial on
+ Isabelle/HOL</a> (published by Springer Verlag as <a href=
+ "http://www4.in.tum.de/~nipkow/LNCS2283/">LNCS 2283</a>) and the <a href=
+ "#course_material">course material</a>.</p>
+ <br clear="both" />
+
+ <h2>Mailing list and FAQ</h2>
+
+ <p>You may use the mailing list <a href=
+ "mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> and its
+ <a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to discuss
+ problems and results. To subscribe, <a href=
+ "mailto:lcp@cl.cam.ac.uk?subject=subscribe&body=Please%20add%20me%20to%20the%20Isabelle%20mailing%20list">
+ contact Larry Paulson</a>.</p>
+ <p>Please consult the <a href="http://isabelle.in.tum.de/faq.html">FAQ</a> for answers to frequent
+ problems.</p>
+
+ <h2>Isabelle Documentation</h2>
+
+ <p><?value key="distname"?> documentation is
+ included here as browsable PDF for convenience. These documents are also part
+ of the standard Isabelle distribution.</p>
+
+ <?include file="//include/documentationdist.include.html"?>
+
+ <h3>Release notes</h3>
+
+ <ul>
+ <li><a href="//dist/packages/Isabelle/ANNOUNCE">ANNOUNCE</a></li>
+ <li><a href="//dist/packages/Isabelle/README.html">README</a></li>
+ <li><a href="//dist/packages/Isabelle/INSTALL">INSTALL</a></li>
+ <li><a href="//dist/packages/Isabelle/NEWS">NEWS</a></li>
+ </ul>
+
+ <h2 id="course_material">Course Material and Exercises</h2>
+ <p>The <a href=
+ "http://isabelle.in.tum.de/coursematerial/">course material</a> page makes
+ slides, demos, and exercises of a growing number of Isabelle courses
+ available. It is meant as a resource for people who would like to learn
+ Isabelle as well as for those who would like to teach it.</p>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="//include/footer.include.html"?>
+</body>
+
+</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dist/download.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,51 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Download</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="dist">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation_dist.include.html"?>
+ <div class="hr"><hr/></div>
+ <div id="content">
+
+ <h2><?value key="distname"?></h2>
+
+ <p>The following source and binary packages of <?value key="distname"?>
+ provide everything required for easy installation of the full Isabelle
+ working environment on common Unix platforms (e.g. Linux, Darwin,
+ Solaris). We provide a complete set of packages for Isabelle, Proof
+ General, and PolyML.</p>
+
+ <p>While XEmacs 21 is not included here, most operating system
+ distributions already provide a suitable package. Some of the
+ packages below are platform dependent; we include binaries for
+ Linux/x86, Solaris/Sparc, and Darwin/PPC (MacOS X).</p>
+
+ <p>Please see the <a href="installation.html">installation instructions</a>
+ for which packages to download and for more information.</p>
+
+ <?include file="//include/downloadtable.include.html"?>
+
+ <h2>Development snapshot</h2>
+
+ <p>For the curious we provide a nightly generated
+ CVS <a href="http://isabelle.in.tum.de/devel/">development snapshot</a> of
+ Isabelle.</p>
+
+ <h2>Past releases</h2>
+
+ <p>Past releases are available from the <a href="download_past.html">archive</a>.</p>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="//include/footer.include.html"?>
+</body>
+
+</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dist/download_past.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,43 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Older Isabelle Releases</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="dist">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation_dist.include.html"?>
+ <div class="hr"><hr/></div>
+ <div id="content">
+
+ <h2>Archive</h2>
+
+ Past releases of Isabelle are available from the Cambridge
+ archive:
+
+<ul>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle2003.tar.gz">Isabelle2003</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle2002.tar.gz">Isabelle2002</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99-2.tar.gz">Isabelle99-2</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99-1.tar.gz">Isabelle99-1</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99.tar.gz">Isabelle99</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle98-1.tar.gz">Isabelle98-1</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle98.tar.gz">Isabelle98</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-8.tar.gz">Isabelle94-8</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-7.tar.gz">Isabelle94-7</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-6.tar.gz">Isabelle94-6</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94.tar.gz">Isabelle94</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle93.tar.gz">Isabelle93</a></li>
+</ul>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="//include/footer.include.html"?>
+</body>
+
+</html>
Binary file Admin/website/dist/img/favicon.ico has changed
Binary file Admin/website/dist/img/isabelle_logo.gif has changed
Binary file Admin/website/dist/img/screenshot_isabelle_macos.gif has changed
Binary file Admin/website/dist/img/tutorial_cover_big.gif has changed
Binary file Admin/website/dist/img/tutorial_cover_small.gif has changed
Binary file Admin/website/dist/img/univ_cambridge.gif has changed
Binary file Admin/website/dist/img/univ_tum.gif has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dist/index.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,38 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Isabelle download mirrors</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="dist">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation_dist.include.html"?>
+ <div class="hr"><hr/></div>
+ <div id="content">
+ <h2>Welcome to the Isabelle Distribution!</h2>
+
+ <p>First, you might like to switch to a nearby mirror:</p>
+
+ <ul>
+ <li><a href=
+ "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/download.html">Cambridge
+ (UK)</a></li>
+
+ <li><a href="http://isabelle.in.tum.de/dist/download.html">Munich
+ (Germany)</a></li>
+
+ <li><a href=
+ "http://mirror.cse.unsw.edu.au/pub/isabelle/download.html">Sydney
+ (Australia)</a></li>
+ </ul>
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="//include/footer.include.html"?>
+</body>
+
+</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dist/installation.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,104 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Installation instructions</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="dist">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation_dist.include.html"?>
+ <div class="hr"><hr/></div>
+ <div id="content">
+
+ <h2>Prerequisites</h2>
+
+ <p>Isabelle runs on common Unix platforms (Linux, Solaris, etc.).
+ Below we provide also some <a href="#other_platforms">hints</a>
+ on how to use Isabelle on other, not-quite-Unix platforms.</p>
+
+ <p>
+ The packages available from our <a href="download.html">download page</a>
+ expect the following software to be installed:
+ </p>
+
+ <ul>
+ <li>bash 1.x or 2.x</li>
+ <li>Perl 5.x</li>
+ <li>optionally, XEmacs 21 or Emacs 21 with mule support (for ProofGeneral)</li>
+ <li>optionally, Java 1.1 or above (for theory graph browsing)</li>
+ </ul>
+
+ <p>
+ Our download page includes packages for a suitable implementation of Standard ML
+ (<a href="http://www.polyml.org">Poly/ML</a>) and
+ <a
+ href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a>
+ (please <a
+ href="http://proofgeneral.inf.ed.ac.uk/register">register</a>). The
+ Proof General distribution now already includes the <a
+ href="http://x-symbol.sourceforge.net">X-Symbol</a> package,
+ there is no need to download it separately.
+ </p>
+
+ <h2>Installation</h2>
+
+ <p>In fact, there is no
+ installation required. Users may just unpack all required packages within the
+ same directory. The default settings of Isabelle should be reasonable for
+ most circumstances.</p>
+
+ <p>A typical Linux/x86 site installation of Isabelle/HOL works as follows:</p>
+ <ul>
+ <li>By using GNU <tt>tar</tt>, the archives are uncompressed and unpacked into the
+ <tt>/usr/local</tt> directory (this location may be changed to anything
+ appropriate):
+ <blockquote>
+ <tt>tar -C /usr/local -xzf <?value key="distname"?>.tar.gz</tt><br />
+ <tt>tar -C /usr/local -xzf ProofGeneral.tar.gz</tt><br />
+ <tt>tar -C /usr/local -xzf polyml_base.tar.gz</tt><br />
+ <tt>tar -C /usr/local -xzf polyml_x86-linux.tar.gz</tt><br />
+ <tt>tar -C /usr/local -xzf HOL_x86-linux.tar.gz</tt><br />
+ </blockquote>
+ </li>
+ <li>
+ Users may now invoke Isabelle without further ado, e.g. run the main
+ executable <tt>/usr/local/Isabelle/bin/Isabelle</tt> to launch the Proof
+ General interface for Isabelle/Isar. Note that there is a separate option in
+ the Proof General <em>Options</em> menu to enable X-Symbol.
+ </li>
+ <li>If Emacs appears to hang when the prover process is started, see the
+ <a href="http://proofgeneral.inf.ed.ac.uk/FAQ">ProofGeneral FAQ</a> for
+ advice.
+ </li>
+ </ul>
+
+ <p>For more information, see the file <a href="../isabelle/Isabelle/INSTALL">INSTALL</a> included in
+ <?value key="distname"?>.tar.gz.</p>
+
+ <h2 id="other_platforms">Other platforms</h2>
+
+ <p>Although Isabelle is natively designed for Unix environments,
+ it may also run under similar, Unix-like platforms. The
+ following installation instructions are hints contributed by
+ Isabelle users. Please feel free to contact us for any suggestions,
+ corrections or improvements.</p>
+
+ <ul>
+ <li><a href="installation_notes_macosx.html">Installation notes for Mac OS
+ X</a></li>
+
+ <li><a href="installation_notes_cygwin.html">Installation notes for
+ Cygwin/Windows</a></li>
+ </ul>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="../include/footer.include.html"?>
+</body>
+
+</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dist/installation_notes_cygwin.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,265 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Installation notes for Windows/Cygwin</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="dist">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation_dist.include.html"?>
+ <div class="hr"><hr/></div>
+ <div id="content">
+
+ <h2>Preconditions and restrictions</h2>
+
+ <p>Please notice before you go ahead:</p>
+
+ <ul>
+ <li>The ML system these notes apply to is <a href=
+ "http://www.smlnj.org/">Standard ML of New Jersey</a>; it is <em>not</em>
+ known yet how to get Isabelle run completely with <a href=
+ "www.polyml.org/">Poly/ML</a>. See <a href="#polyml">a note on Poly/ML</a>
+ down this page.</li>
+
+ <li>It is assumed you have some experience with an Unix operating system
+ (e.g. what a shell is for and how to use it).</li>
+ </ul>
+
+ <h2>Acknowlegements</h2>
+
+ <p>Thanks to <a href=
+ "http://cswww.essex.ac.uk/Research/FSS/projects/isawin/">Norbert
+ Völker</a> and <a href=
+ "http://www.abo.fi/~viorel.preoteasa/isabelle/">Viorel Preoteasa</a> whose
+ efforts helped a lot to get Isabelle run this way.</p>
+
+ <h2>Installing Cygwin</h2>
+
+ <p>Cygwin is a POSIX emulation layer for Windows; it contains ports of a
+ large collection of common Unix software (shells, perl, gcc, X11, latex,
+ ImageMagick, …).</p>
+
+ <p>To install it, get the installer from the <a href=
+ "http://www.cygwin.com">Cygwin website</a> and run it. It will ask you which
+ packages to install, and then downloads and installs them. Please make sure
+ you install everything needed by Isabelle; it is hard to give a concise list
+ of packages here since the bundling of Cygwin packages may vary over time,
+ but installing the base packages, perl, make, xemacs and x-server should be a
+ good choice for the beginning.</p>
+
+ <p>By default, cygwin installs to <tt>c:\cygwin</tt>; you may choose an
+ arbitrary location, but it is recommended that it does not include any space
+ or exotic characters. This directory will then become the root directory of
+ the Cygwin filesystem tree, i.e. the Cygwin path <tt>/opt/smlnj</tt> will be
+ mapped to Windows path <tt>c:\cygwin\opt\smlnj</tt>.</p>
+
+ <p>After installation, open a Cygwin shell window (normally the installer
+ makes a shortcut for you).</p>
+
+ <h2>Getting and building SML/NJ</h2>
+
+ <p>Now we are ready to get and build <a href=
+ "http://www.smlnj.org/">SML/NJ</a>; before this, set the environment variable
+ SMLNJ_CYGWIN_RUNTIME to 1:</p>
+
+ <blockquote>
+ <tt>export SMLNJ_CYGWIN_RUNTIME=1</tt>
+ </blockquote>
+
+ <blockquote>
+ (or <tt>setenv SMLNJ_CYGWIN_RUNTIME 1</tt> for c shells).
+ </blockquote>
+
+ <p>This setting will tell the build process that it should
+ <em>not</em> attempt to build SML/NJ natively for Win32 but for Cygwin
+ instead (see further <a href=
+ "http://smlnj.cs.uchicago.edu/dist/working/110.53/CYGWININSTALL">CYGWININSTALL</a>).</p>
+
+ <p>So far, this setup was tested using the working version 110.53 of SML/NJ
+ from <a href=
+ "http://smlnj.cs.uchicago.edu/dist/working/110.53/">http://smlnj.cs.uchicago.edu/dist/working/110.53/</a>.
+ SML/NJ provides a nice installer enabling you to download and build it. Read
+ <a href=
+ "http://smlnj.cs.uchicago.edu/dist/working/110.53/INSTALL">INSTALL</a> to
+ learn about the different possibilites to do this. The default packages
+ should be sufficient.</p>
+
+ <p>In the following, it is assumed that you install SML/NJ to Cygwin path
+ <tt>/opt/smlnj</tt>; if you choose an other location, some tweaking in the
+ <a href="#config"><tt>etc/settings</tt> file</a> may be neccessary later.</p>
+
+ <p>Whenever SMLNJ is used, the SMLNJ_CYGWIN_RUNTIME environment variable must
+ be set to 1 (later on a convenient mechanism to make this the default is
+ proposed).</p>
+
+ <h2>Installing Isabelle</h2>
+
+ <p>Download the latest Isabelle and ProofGeneral <a href=
+ "packages.html">release packages</a>. Assuming that you are in the directory
+ where you downloaded the files, install them into <tt>/opt</tt> by typing
+ into the bash shell:</p>
+
+ <blockquote>
+ <tt>tar -C /usr/opt -xvzf <?value key="distname"?>.tar.gz</tt><br />
+ <tt>tar -C /usr/opt -xvzf ProofGeneral.tar.gz</tt><br />
+ </blockquote>
+
+ <p>During extraction, one inconvenience may occur, see <a href=
+ "inconvenience">below</a>.</p>
+
+ <p>The location <tt>/opt</tt> again is just a proposal; if you choose other
+ locations, some tweaking in the <a href="#config"><tt>etc/settings</tt>
+ file</a> may be neccessary later.</p>
+
+ <h2 id="config">Configuring Isabelle</h2>
+
+ <p>Edit the file <tt>/opt/Isabelle/etc/settings</tt>; first, uncomment the
+ lines about SMLNJ. Also set the variable SMLNJ_CYGWIN_RUNTIME to 1, in order
+ the cygwin version of SMLNJ is used. As mentioned above, the path variables
+ for the ML system and ProofGeneral may need adjustions, depending on your
+ different installation locations.</p>
+
+ <p>Take heed of the setting of ISABELLE_HOME_USER; by default, this is
+ <tt>~/isabelle</tt>. To detect which Windows path this will be mapped to,
+ type into the Cygwin bash shell:</p>
+
+ <blockquote>
+ <tt>cygpath --windows ~/isabelle</tt>
+ </blockquote>
+
+ <p>If you don't like this location to be the isabelle home
+ directory, consider setting of ISABELLE_HOME_USER to another value; use
+ <tt>cygpath --unix <winpath></tt> to detect which Cygwin path a given
+ Windows path is mapped to.</p>
+
+ <p>A typical change could look like this:</p>
+
+ <blockquote>
+ from<br />
+ <tt># Standard ML of New Jersey 110 or later<br />
+ #ML_SYSTEM=smlnj-110<br />
+ #ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
+ #ML_OPTIONS="@SMLdebug=/dev/null"<br />
+ #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
+ "$HEAP_SUFFIX")<br /></tt>
+ </blockquote>
+
+ <blockquote>
+ to<br />
+ <tt># Standard ML of New Jersey 110 or later<br />
+ SMLNJ_CYGWIN_RUNTIME=1<br />
+ ML_SYSTEM=smlnj-110<br />
+ ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
+ ML_OPTIONS="@SMLdebug=/dev/null"<br />
+ ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
+ "$HEAP_SUFFIX")</tt>
+ </blockquote>
+
+ <h2>Building logics</h2>
+
+ <p>Now we can compile some logics. Start the cygwin shell (if not still
+ running) and type:</p>
+
+ <blockquote>
+ <tt>cd /opt/Isabelle</tt><br />
+ <tt>build HOL</tt><br />
+ <tt>build ZF</tt><br />
+ </blockquote>
+
+ <p>The compilation process may take some time (depending on how fast the
+ computer is). Before building a logic image the build program shows some
+ variables and expects user input – just hit enter.</p>
+
+ <h2>Running Isabelle with ProofGeneral</h2>
+
+ <p>On Linux, Isabelle can be started by two scripts located in
+ <tt>Isabelle/bin</tt>: <tt>Isabelle</tt> and <tt>isabelle</tt>.
+ <tt>Isabelle</tt> attempts to start ProofGeneral with XEmacs, and isabelle
+ starts it in an SML shell session. However Windows treats the two names as
+ one. To get around this just copy <tt>/opt/Isabelle/bin/isabelle</tt> to
+ <tt>/opt/Isabelle/bin/Isabell</tt>. The script
+ <tt>/opt/Isabelle/bin/Isabell</tt> will start Isabelle with ProofGeneral.</p>
+
+ <p>Now everything should be ready. To test, start the cygwin shell and
+ type</p>
+
+ <blockquote>
+ <tt>startx &</tt>
+ </blockquote>
+
+ <p>This will start the cygwin X server and an X shell window. In
+ the X shell window, type</p>
+
+ <blockquote>
+ <tt>/opt/Isabelle/bin/Isabell &</tt>.
+ </blockquote>
+
+ <p>This will start the ProofGeneral interface for Isabelle. After a
+ while an empty buffer <tt>Scratch.thy</tt> is created. You can turn on
+ X-Symbol from the menu Proof-General, item Options.</p>
+
+ <p>Load one of your favorite theories and test your Isabelle installation by
+ proving something.</p>
+
+ <p>To simplify starting ProofGeneral, consider writing a Windows command
+ script, e.g.</p>
+
+ <blockquote>
+ <tt>@bash startx -geometry 30x4 -iconic -e Isabell</tt>
+ </blockquote>
+
+ <p>and assigning a shortcut in the start menu to it.</p>
+
+ <h2 id="inconvenience">Inconveniencies with the current version of
+ Isabelle</h2>
+
+ <p>With the current Isabelle release (Isabelle 2004), there are two
+ inconveniencies:</p>
+
+ <ul>
+ <li>During extraction you will get a warning that file
+ <tt>Real/HahnBanach/Aux.thy</tt> can not be created. This is because
+ <tt>Aux</tt> is not allowed as a filename under Windows. If you do not want
+ to run the HahnBanach example, you might simply want to ignore this
+ warning.</li>
+
+ <li>The tool <tt>isatool mkdir</tt> tries to detect the name of the current
+ user, to put it into the generated <tt>root.tex</tt>. Alas, on Windows,
+ this leads to an unquoted <tt>\</tt> in the TeX file. So you either must
+ edit your <tt>root.tex</tt> manually to fix this, or directly patch
+ <tt>/opt/Isabelle/lib/Tools/mkdir</tt> by replacing
+
+ <blockquote>
+ <tt>AUTHOR=$("$AUTO_PERL" -e "@pw = getpwnam(\"$USER\"); print @pw[6]" | tr _ -)</tt>
+ </blockquote>with
+
+ <blockquote>
+ <tt>AUTHOR="default author name"</tt>
+ </blockquote>
+ </li>
+ </ul>
+
+ <p>To get around these inconveniencies, consider using a recent developer
+ snapshot of Isabelle; both will be fixed in the next Isabelle release.</p>
+
+ <h2 id="polyml">A note on Poly/ML</h2>
+
+ <p>As indicated above, Isabelle does <em>not</em> run neatly with <a href=
+ "www.polyml.org/">Poly/ML</a> on Windows, since it is not clear
+ how Poly/ML has to be compiled for Cygwin, and the native Windows port
+ of PolyML do not provide some Posix interfaces Isabelle relies on.</p>
+
+ <p>If you know how to circumvent (fully or partially) any of these problems,
+ please let us know.</p>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="../include/footer.include.html"?>
+</body>
+
+</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dist/installation_notes_macosx.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,120 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Installation hints for Mac OS X</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="dist">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation_dist.include.html"?>
+ <div class="hr"><hr/></div>
+ <div id="content">
+
+ <h2>Installing on Mac OS X</h2>
+ <p><a href="http://www.apple.com/macosx/">Mac OS X</a> is the current version
+ of the Macintosh operating system, installed on all new <a href=
+ "http://www.apple.com/">Apple</a> computers. Because it is based on Unix, it
+ can run <a href=
+ "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">Isabelle</a>. The new
+ <a href="http://www.apple.com/powermac/">Power Mac G5</a> is an excellent
+ Isabelle machine. Here is a <a href=
+ "../img/screenshot_isabelle_macos.jpg">screenshot</a> showing Proof General running
+ in GNU Emacs.</p>
+
+ <p>This page gives advice on building Isabelle for Mac OS X. It assumes that
+ you are familiar with both Mac OS X and Unix. You must have installed the Mac
+ OS X developer tools.</p>
+
+ <ol>
+ <li>Download Isabelle to a suitable directory, as described on the
+ <a href="packages.html">download page</a>. Be sure to get the following
+ files
+
+ <ul>
+ <li><?value key="distname"?>.tar.gz</li>
+ <li>ProofGeneral.tar.gz</li>
+ <li>polyml_base.tar.gz</li>
+ <li>polyml_ppc-darwin.tar.gz</li>
+ <li>HOL_ppc-darwin.tar.gz</li>
+ </ul>
+ </li>
+
+ <li>You may have to install the bash shell. Versions of Mac OS X prior to
+ 10.2.2 did not provide it. If /bin/bash does not exist, you can install it
+ using the package manager <a href=
+ "http://fink.sourceforge.net/">Fink</a>.</li>
+
+ <li>At this point, you should be able to run Isabelle with the command line
+ interface. You can also build Isabelle from the Unix command line,
+ following the instructions for "Compiling Logics" in file
+ <tt>Isabelle/INSTALL.</tt></li>
+
+ <li>You should also be able to launch <a href=
+ "http://proofgeneral.inf.ed.ac.uk/">Proof General</a> by typing
+ "<tt>Isabelle</tt>" at the Unix command line. This will invoke the
+ Apple-supplied version of Emacs in a terminal window, providing a primitive
+ environment. Somewhat better is to run Proof General from within a version
+ of Emacs ported as a native Mac OS X application, such as <a href=
+ "http://home.att.ne.jp/alpha/z123/emacs-mac-e.html">MacEmacs JP</a> or
+ <a href="http://mindlube.com/products/emacs/">mindlube's</a> or <a href=
+ "http://www.cs.man.ac.uk/%7efranconi/mac-emacs/">Enhanced Carbon Emacs</a>.
+ Visiting a theory file from Emacs will automatically launch Proof General
+ provided <tt>isabelle</tt> is on the search path. None of these options
+ support the X-Symbol package, unfortunately.</li>
+ </ol>
+
+ <p>In order to get the full benefit of Proof General, you must install the X
+ Window System (X11) and <a href="http://www.xemacs.org/">XEmacs</a> or
+ <a href="http://www.gnu.org/software/emacs/emacs.html">GNU Emacs</a>.</p>
+
+ <ul>
+ <li><a href="http://www.apple.com/macosx/x11/">Apple's version</a> of X11
+ is included with the Panther (MacOS 10.3) installation discs, though it is
+ not installed by default. The Command key serves as Meta, but it is
+ reserved for standard Apple shortcuts such as C, V and X, so you must use
+ Esc-C, Esc-V and Esc-X in Emacs or else deselect "Enable key equivalents"
+ in the X11 preferences.</li>
+
+ <li>Some people prefer the <a href=
+ "http://www.osxgnu.org/software/Xwin/WindowManagers/OroborOSX/">OroborOSX</a>
+ window manager. It must be used in conjunction with <a href=
+ "http://xfree86.org/">XFree86</a>, which is easy to install if you use the
+ installer provided by the <a href=
+ "http://sourceforge.net/projects/xonx/">XonX</a> project.</li>
+ </ul>
+
+ <p>The easiest way to install XEmacs or GNU Emacs is via the package manager
+ <a href="http://fink.sourceforge.net/">Fink</a>. Install the Fink package
+ <tt>xemacs-sumo-pkg</tt> to get the XEmacs libraries that Proof General needs
+ to run. To install GNU Emacs, install the package <tt>emacs21</tt>. Fink can
+ compile from sources, but this takes hours, so it is better to request binary
+ installations.</p>
+
+ <p>To use <a href="http://www.gnu.org/software/emacs/emacs.html">GNU
+ Emacs</a> instead of <a href="http://www.xemacs.org/">XEmacs</a>, you must
+ recompile Proof General and X-Symbol following the instructions <a href=
+ "http://proofgeneral.inf.ed.ac.uk/FAQ">here</a>. Note that Proof General
+ incorporates its own copy of X-Symbol.</p>
+
+ <ol>
+ <li>Install X11 or OroborOSX.</li>
+
+ <li>Install XEmacs (and its libraries), or install GNU Emacs and recompile
+ Proof General.</li>
+
+ <li>You may want to install this drag-and-drop <a href=
+ "IsabelleDroplet.dmg">Isabelle launcher</a>. It is a simple hack that
+ invokes xemacs on any files dropped on it.</li>
+ </ol>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="../include/footer.include.html"?>
+</body>
+
+</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dist/others.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,35 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Other Isabelle resources</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="dist">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation_dist.include.html"?>
+ <div class="hr"><hr/></div>
+ <div id="content">
+ <h2>More about Isabelle</h2>
+
+ <p>is available on our main pages</p>
+
+ <ul>
+ <li>at <a href=
+ "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html">Cambridge
+ (UK)</a></li>
+
+ <li>at <a href="http://isabelle.in.tum.de/index.html">Munich
+ (Germany)</a></li>
+ </ul>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="//include/footer.include.html"?>
+</body>
+
+</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dtd/xhtml-lat1.ent Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,196 @@
+<!-- Portions (C) International Organization for Standardization 1986
+ Permission to copy in any form is granted for use with
+ conforming SGML systems and applications as defined in
+ ISO 8879, provided this notice is included in all copies.
+-->
+<!-- Character entity set. Typical invocation:
+ <!ENTITY % HTMLlat1 PUBLIC
+ "-//W3C//ENTITIES Latin 1 for XHTML//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml-lat1.ent">
+ %HTMLlat1;
+-->
+
+<!ENTITY nbsp " "> <!-- no-break space = non-breaking space,
+ U+00A0 ISOnum -->
+<!ENTITY iexcl "¡"> <!-- inverted exclamation mark, U+00A1 ISOnum -->
+<!ENTITY cent "¢"> <!-- cent sign, U+00A2 ISOnum -->
+<!ENTITY pound "£"> <!-- pound sign, U+00A3 ISOnum -->
+<!ENTITY curren "¤"> <!-- currency sign, U+00A4 ISOnum -->
+<!ENTITY yen "¥"> <!-- yen sign = yuan sign, U+00A5 ISOnum -->
+<!ENTITY brvbar "¦"> <!-- broken bar = broken vertical bar,
+ U+00A6 ISOnum -->
+<!ENTITY sect "§"> <!-- section sign, U+00A7 ISOnum -->
+<!ENTITY uml "¨"> <!-- diaeresis = spacing diaeresis,
+ U+00A8 ISOdia -->
+<!ENTITY copy "©"> <!-- copyright sign, U+00A9 ISOnum -->
+<!ENTITY ordf "ª"> <!-- feminine ordinal indicator, U+00AA ISOnum -->
+<!ENTITY laquo "«"> <!-- left-pointing double angle quotation mark
+ = left pointing guillemet, U+00AB ISOnum -->
+<!ENTITY not "¬"> <!-- not sign = angled dash,
+ U+00AC ISOnum -->
+<!ENTITY shy "­"> <!-- soft hyphen = discretionary hyphen,
+ U+00AD ISOnum -->
+<!ENTITY reg "®"> <!-- registered sign = registered trade mark sign,
+ U+00AE ISOnum -->
+<!ENTITY macr "¯"> <!-- macron = spacing macron = overline
+ = APL overbar, U+00AF ISOdia -->
+<!ENTITY deg "°"> <!-- degree sign, U+00B0 ISOnum -->
+<!ENTITY plusmn "±"> <!-- plus-minus sign = plus-or-minus sign,
+ U+00B1 ISOnum -->
+<!ENTITY sup2 "²"> <!-- superscript two = superscript digit two
+ = squared, U+00B2 ISOnum -->
+<!ENTITY sup3 "³"> <!-- superscript three = superscript digit three
+ = cubed, U+00B3 ISOnum -->
+<!ENTITY acute "´"> <!-- acute accent = spacing acute,
+ U+00B4 ISOdia -->
+<!ENTITY micro "µ"> <!-- micro sign, U+00B5 ISOnum -->
+<!ENTITY para "¶"> <!-- pilcrow sign = paragraph sign,
+ U+00B6 ISOnum -->
+<!ENTITY middot "·"> <!-- middle dot = Georgian comma
+ = Greek middle dot, U+00B7 ISOnum -->
+<!ENTITY cedil "¸"> <!-- cedilla = spacing cedilla, U+00B8 ISOdia -->
+<!ENTITY sup1 "¹"> <!-- superscript one = superscript digit one,
+ U+00B9 ISOnum -->
+<!ENTITY ordm "º"> <!-- masculine ordinal indicator,
+ U+00BA ISOnum -->
+<!ENTITY raquo "»"> <!-- right-pointing double angle quotation mark
+ = right pointing guillemet, U+00BB ISOnum -->
+<!ENTITY frac14 "¼"> <!-- vulgar fraction one quarter
+ = fraction one quarter, U+00BC ISOnum -->
+<!ENTITY frac12 "½"> <!-- vulgar fraction one half
+ = fraction one half, U+00BD ISOnum -->
+<!ENTITY frac34 "¾"> <!-- vulgar fraction three quarters
+ = fraction three quarters, U+00BE ISOnum -->
+<!ENTITY iquest "¿"> <!-- inverted question mark
+ = turned question mark, U+00BF ISOnum -->
+<!ENTITY Agrave "À"> <!-- latin capital letter A with grave
+ = latin capital letter A grave,
+ U+00C0 ISOlat1 -->
+<!ENTITY Aacute "Á"> <!-- latin capital letter A with acute,
+ U+00C1 ISOlat1 -->
+<!ENTITY Acirc "Â"> <!-- latin capital letter A with circumflex,
+ U+00C2 ISOlat1 -->
+<!ENTITY Atilde "Ã"> <!-- latin capital letter A with tilde,
+ U+00C3 ISOlat1 -->
+<!ENTITY Auml "Ä"> <!-- latin capital letter A with diaeresis,
+ U+00C4 ISOlat1 -->
+<!ENTITY Aring "Å"> <!-- latin capital letter A with ring above
+ = latin capital letter A ring,
+ U+00C5 ISOlat1 -->
+<!ENTITY AElig "Æ"> <!-- latin capital letter AE
+ = latin capital ligature AE,
+ U+00C6 ISOlat1 -->
+<!ENTITY Ccedil "Ç"> <!-- latin capital letter C with cedilla,
+ U+00C7 ISOlat1 -->
+<!ENTITY Egrave "È"> <!-- latin capital letter E with grave,
+ U+00C8 ISOlat1 -->
+<!ENTITY Eacute "É"> <!-- latin capital letter E with acute,
+ U+00C9 ISOlat1 -->
+<!ENTITY Ecirc "Ê"> <!-- latin capital letter E with circumflex,
+ U+00CA ISOlat1 -->
+<!ENTITY Euml "Ë"> <!-- latin capital letter E with diaeresis,
+ U+00CB ISOlat1 -->
+<!ENTITY Igrave "Ì"> <!-- latin capital letter I with grave,
+ U+00CC ISOlat1 -->
+<!ENTITY Iacute "Í"> <!-- latin capital letter I with acute,
+ U+00CD ISOlat1 -->
+<!ENTITY Icirc "Î"> <!-- latin capital letter I with circumflex,
+ U+00CE ISOlat1 -->
+<!ENTITY Iuml "Ï"> <!-- latin capital letter I with diaeresis,
+ U+00CF ISOlat1 -->
+<!ENTITY ETH "Ð"> <!-- latin capital letter ETH, U+00D0 ISOlat1 -->
+<!ENTITY Ntilde "Ñ"> <!-- latin capital letter N with tilde,
+ U+00D1 ISOlat1 -->
+<!ENTITY Ograve "Ò"> <!-- latin capital letter O with grave,
+ U+00D2 ISOlat1 -->
+<!ENTITY Oacute "Ó"> <!-- latin capital letter O with acute,
+ U+00D3 ISOlat1 -->
+<!ENTITY Ocirc "Ô"> <!-- latin capital letter O with circumflex,
+ U+00D4 ISOlat1 -->
+<!ENTITY Otilde "Õ"> <!-- latin capital letter O with tilde,
+ U+00D5 ISOlat1 -->
+<!ENTITY Ouml "Ö"> <!-- latin capital letter O with diaeresis,
+ U+00D6 ISOlat1 -->
+<!ENTITY times "×"> <!-- multiplication sign, U+00D7 ISOnum -->
+<!ENTITY Oslash "Ø"> <!-- latin capital letter O with stroke
+ = latin capital letter O slash,
+ U+00D8 ISOlat1 -->
+<!ENTITY Ugrave "Ù"> <!-- latin capital letter U with grave,
+ U+00D9 ISOlat1 -->
+<!ENTITY Uacute "Ú"> <!-- latin capital letter U with acute,
+ U+00DA ISOlat1 -->
+<!ENTITY Ucirc "Û"> <!-- latin capital letter U with circumflex,
+ U+00DB ISOlat1 -->
+<!ENTITY Uuml "Ü"> <!-- latin capital letter U with diaeresis,
+ U+00DC ISOlat1 -->
+<!ENTITY Yacute "Ý"> <!-- latin capital letter Y with acute,
+ U+00DD ISOlat1 -->
+<!ENTITY THORN "Þ"> <!-- latin capital letter THORN,
+ U+00DE ISOlat1 -->
+<!ENTITY szlig "ß"> <!-- latin small letter sharp s = ess-zed,
+ U+00DF ISOlat1 -->
+<!ENTITY agrave "à"> <!-- latin small letter a with grave
+ = latin small letter a grave,
+ U+00E0 ISOlat1 -->
+<!ENTITY aacute "á"> <!-- latin small letter a with acute,
+ U+00E1 ISOlat1 -->
+<!ENTITY acirc "â"> <!-- latin small letter a with circumflex,
+ U+00E2 ISOlat1 -->
+<!ENTITY atilde "ã"> <!-- latin small letter a with tilde,
+ U+00E3 ISOlat1 -->
+<!ENTITY auml "ä"> <!-- latin small letter a with diaeresis,
+ U+00E4 ISOlat1 -->
+<!ENTITY aring "å"> <!-- latin small letter a with ring above
+ = latin small letter a ring,
+ U+00E5 ISOlat1 -->
+<!ENTITY aelig "æ"> <!-- latin small letter ae
+ = latin small ligature ae, U+00E6 ISOlat1 -->
+<!ENTITY ccedil "ç"> <!-- latin small letter c with cedilla,
+ U+00E7 ISOlat1 -->
+<!ENTITY egrave "è"> <!-- latin small letter e with grave,
+ U+00E8 ISOlat1 -->
+<!ENTITY eacute "é"> <!-- latin small letter e with acute,
+ U+00E9 ISOlat1 -->
+<!ENTITY ecirc "ê"> <!-- latin small letter e with circumflex,
+ U+00EA ISOlat1 -->
+<!ENTITY euml "ë"> <!-- latin small letter e with diaeresis,
+ U+00EB ISOlat1 -->
+<!ENTITY igrave "ì"> <!-- latin small letter i with grave,
+ U+00EC ISOlat1 -->
+<!ENTITY iacute "í"> <!-- latin small letter i with acute,
+ U+00ED ISOlat1 -->
+<!ENTITY icirc "î"> <!-- latin small letter i with circumflex,
+ U+00EE ISOlat1 -->
+<!ENTITY iuml "ï"> <!-- latin small letter i with diaeresis,
+ U+00EF ISOlat1 -->
+<!ENTITY eth "ð"> <!-- latin small letter eth, U+00F0 ISOlat1 -->
+<!ENTITY ntilde "ñ"> <!-- latin small letter n with tilde,
+ U+00F1 ISOlat1 -->
+<!ENTITY ograve "ò"> <!-- latin small letter o with grave,
+ U+00F2 ISOlat1 -->
+<!ENTITY oacute "ó"> <!-- latin small letter o with acute,
+ U+00F3 ISOlat1 -->
+<!ENTITY ocirc "ô"> <!-- latin small letter o with circumflex,
+ U+00F4 ISOlat1 -->
+<!ENTITY otilde "õ"> <!-- latin small letter o with tilde,
+ U+00F5 ISOlat1 -->
+<!ENTITY ouml "ö"> <!-- latin small letter o with diaeresis,
+ U+00F6 ISOlat1 -->
+<!ENTITY divide "÷"> <!-- division sign, U+00F7 ISOnum -->
+<!ENTITY oslash "ø"> <!-- latin small letter o with stroke,
+ = latin small letter o slash,
+ U+00F8 ISOlat1 -->
+<!ENTITY ugrave "ù"> <!-- latin small letter u with grave,
+ U+00F9 ISOlat1 -->
+<!ENTITY uacute "ú"> <!-- latin small letter u with acute,
+ U+00FA ISOlat1 -->
+<!ENTITY ucirc "û"> <!-- latin small letter u with circumflex,
+ U+00FB ISOlat1 -->
+<!ENTITY uuml "ü"> <!-- latin small letter u with diaeresis,
+ U+00FC ISOlat1 -->
+<!ENTITY yacute "ý"> <!-- latin small letter y with acute,
+ U+00FD ISOlat1 -->
+<!ENTITY thorn "þ"> <!-- latin small letter thorn,
+ U+00FE ISOlat1 -->
+<!ENTITY yuml "ÿ"> <!-- latin small letter y with diaeresis,
+ U+00FF ISOlat1 -->
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dtd/xhtml-special.ent Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,80 @@
+<!-- Special characters for XHTML -->
+
+<!-- Character entity set. Typical invocation:
+ <!ENTITY % HTMLspecial PUBLIC
+ "-//W3C//ENTITIES Special for XHTML//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml-special.ent">
+ %HTMLspecial;
+-->
+
+<!-- Portions (C) International Organization for Standardization 1986:
+ Permission to copy in any form is granted for use with
+ conforming SGML systems and applications as defined in
+ ISO 8879, provided this notice is included in all copies.
+-->
+
+<!-- Relevant ISO entity set is given unless names are newly introduced.
+ New names (i.e., not in ISO 8879 list) do not clash with any
+ existing ISO 8879 entity names. ISO 10646 character numbers
+ are given for each character, in hex. values are decimal
+ conversions of the ISO 10646 values and refer to the document
+ character set. Names are Unicode names.
+-->
+
+<!-- C0 Controls and Basic Latin -->
+<!ENTITY quot """> <!-- quotation mark, U+0022 ISOnum -->
+<!ENTITY amp "&#38;"> <!-- ampersand, U+0026 ISOnum -->
+<!ENTITY lt "&#60;"> <!-- less-than sign, U+003C ISOnum -->
+<!ENTITY gt ">"> <!-- greater-than sign, U+003E ISOnum -->
+<!ENTITY apos "'"> <!-- apostrophe = APL quote, U+0027 ISOnum -->
+
+<!-- Latin Extended-A -->
+<!ENTITY OElig "Œ"> <!-- latin capital ligature OE,
+ U+0152 ISOlat2 -->
+<!ENTITY oelig "œ"> <!-- latin small ligature oe, U+0153 ISOlat2 -->
+<!-- ligature is a misnomer, this is a separate character in some languages -->
+<!ENTITY Scaron "Š"> <!-- latin capital letter S with caron,
+ U+0160 ISOlat2 -->
+<!ENTITY scaron "š"> <!-- latin small letter s with caron,
+ U+0161 ISOlat2 -->
+<!ENTITY Yuml "Ÿ"> <!-- latin capital letter Y with diaeresis,
+ U+0178 ISOlat2 -->
+
+<!-- Spacing Modifier Letters -->
+<!ENTITY circ "ˆ"> <!-- modifier letter circumflex accent,
+ U+02C6 ISOpub -->
+<!ENTITY tilde "˜"> <!-- small tilde, U+02DC ISOdia -->
+
+<!-- General Punctuation -->
+<!ENTITY ensp " "> <!-- en space, U+2002 ISOpub -->
+<!ENTITY emsp " "> <!-- em space, U+2003 ISOpub -->
+<!ENTITY thinsp " "> <!-- thin space, U+2009 ISOpub -->
+<!ENTITY zwnj "‌"> <!-- zero width non-joiner,
+ U+200C NEW RFC 2070 -->
+<!ENTITY zwj "‍"> <!-- zero width joiner, U+200D NEW RFC 2070 -->
+<!ENTITY lrm "‎"> <!-- left-to-right mark, U+200E NEW RFC 2070 -->
+<!ENTITY rlm "‏"> <!-- right-to-left mark, U+200F NEW RFC 2070 -->
+<!ENTITY ndash "–"> <!-- en dash, U+2013 ISOpub -->
+<!ENTITY mdash "—"> <!-- em dash, U+2014 ISOpub -->
+<!ENTITY lsquo "‘"> <!-- left single quotation mark,
+ U+2018 ISOnum -->
+<!ENTITY rsquo "’"> <!-- right single quotation mark,
+ U+2019 ISOnum -->
+<!ENTITY sbquo "‚"> <!-- single low-9 quotation mark, U+201A NEW -->
+<!ENTITY ldquo "“"> <!-- left double quotation mark,
+ U+201C ISOnum -->
+<!ENTITY rdquo "”"> <!-- right double quotation mark,
+ U+201D ISOnum -->
+<!ENTITY bdquo "„"> <!-- double low-9 quotation mark, U+201E NEW -->
+<!ENTITY dagger "†"> <!-- dagger, U+2020 ISOpub -->
+<!ENTITY Dagger "‡"> <!-- double dagger, U+2021 ISOpub -->
+<!ENTITY permil "‰"> <!-- per mille sign, U+2030 ISOtech -->
+<!ENTITY lsaquo "‹"> <!-- single left-pointing angle quotation mark,
+ U+2039 ISO proposed -->
+<!-- lsaquo is proposed but not yet ISO standardized -->
+<!ENTITY rsaquo "›"> <!-- single right-pointing angle quotation mark,
+ U+203A ISO proposed -->
+<!-- rsaquo is proposed but not yet ISO standardized -->
+
+<!-- Currency Symbols -->
+<!ENTITY euro "€"> <!-- euro sign, U+20AC NEW -->
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dtd/xhtml-symbol.ent Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,237 @@
+<!-- Mathematical, Greek and Symbolic characters for XHTML -->
+
+<!-- Character entity set. Typical invocation:
+ <!ENTITY % HTMLsymbol PUBLIC
+ "-//W3C//ENTITIES Symbols for XHTML//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml-symbol.ent">
+ %HTMLsymbol;
+-->
+
+<!-- Portions (C) International Organization for Standardization 1986:
+ Permission to copy in any form is granted for use with
+ conforming SGML systems and applications as defined in
+ ISO 8879, provided this notice is included in all copies.
+-->
+
+<!-- Relevant ISO entity set is given unless names are newly introduced.
+ New names (i.e., not in ISO 8879 list) do not clash with any
+ existing ISO 8879 entity names. ISO 10646 character numbers
+ are given for each character, in hex. values are decimal
+ conversions of the ISO 10646 values and refer to the document
+ character set. Names are Unicode names.
+-->
+
+<!-- Latin Extended-B -->
+<!ENTITY fnof "ƒ"> <!-- latin small letter f with hook = function
+ = florin, U+0192 ISOtech -->
+
+<!-- Greek -->
+<!ENTITY Alpha "Α"> <!-- greek capital letter alpha, U+0391 -->
+<!ENTITY Beta "Β"> <!-- greek capital letter beta, U+0392 -->
+<!ENTITY Gamma "Γ"> <!-- greek capital letter gamma,
+ U+0393 ISOgrk3 -->
+<!ENTITY Delta "Δ"> <!-- greek capital letter delta,
+ U+0394 ISOgrk3 -->
+<!ENTITY Epsilon "Ε"> <!-- greek capital letter epsilon, U+0395 -->
+<!ENTITY Zeta "Ζ"> <!-- greek capital letter zeta, U+0396 -->
+<!ENTITY Eta "Η"> <!-- greek capital letter eta, U+0397 -->
+<!ENTITY Theta "Θ"> <!-- greek capital letter theta,
+ U+0398 ISOgrk3 -->
+<!ENTITY Iota "Ι"> <!-- greek capital letter iota, U+0399 -->
+<!ENTITY Kappa "Κ"> <!-- greek capital letter kappa, U+039A -->
+<!ENTITY Lambda "Λ"> <!-- greek capital letter lamda,
+ U+039B ISOgrk3 -->
+<!ENTITY Mu "Μ"> <!-- greek capital letter mu, U+039C -->
+<!ENTITY Nu "Ν"> <!-- greek capital letter nu, U+039D -->
+<!ENTITY Xi "Ξ"> <!-- greek capital letter xi, U+039E ISOgrk3 -->
+<!ENTITY Omicron "Ο"> <!-- greek capital letter omicron, U+039F -->
+<!ENTITY Pi "Π"> <!-- greek capital letter pi, U+03A0 ISOgrk3 -->
+<!ENTITY Rho "Ρ"> <!-- greek capital letter rho, U+03A1 -->
+<!-- there is no Sigmaf, and no U+03A2 character either -->
+<!ENTITY Sigma "Σ"> <!-- greek capital letter sigma,
+ U+03A3 ISOgrk3 -->
+<!ENTITY Tau "Τ"> <!-- greek capital letter tau, U+03A4 -->
+<!ENTITY Upsilon "Υ"> <!-- greek capital letter upsilon,
+ U+03A5 ISOgrk3 -->
+<!ENTITY Phi "Φ"> <!-- greek capital letter phi,
+ U+03A6 ISOgrk3 -->
+<!ENTITY Chi "Χ"> <!-- greek capital letter chi, U+03A7 -->
+<!ENTITY Psi "Ψ"> <!-- greek capital letter psi,
+ U+03A8 ISOgrk3 -->
+<!ENTITY Omega "Ω"> <!-- greek capital letter omega,
+ U+03A9 ISOgrk3 -->
+
+<!ENTITY alpha "α"> <!-- greek small letter alpha,
+ U+03B1 ISOgrk3 -->
+<!ENTITY beta "β"> <!-- greek small letter beta, U+03B2 ISOgrk3 -->
+<!ENTITY gamma "γ"> <!-- greek small letter gamma,
+ U+03B3 ISOgrk3 -->
+<!ENTITY delta "δ"> <!-- greek small letter delta,
+ U+03B4 ISOgrk3 -->
+<!ENTITY epsilon "ε"> <!-- greek small letter epsilon,
+ U+03B5 ISOgrk3 -->
+<!ENTITY zeta "ζ"> <!-- greek small letter zeta, U+03B6 ISOgrk3 -->
+<!ENTITY eta "η"> <!-- greek small letter eta, U+03B7 ISOgrk3 -->
+<!ENTITY theta "θ"> <!-- greek small letter theta,
+ U+03B8 ISOgrk3 -->
+<!ENTITY iota "ι"> <!-- greek small letter iota, U+03B9 ISOgrk3 -->
+<!ENTITY kappa "κ"> <!-- greek small letter kappa,
+ U+03BA ISOgrk3 -->
+<!ENTITY lambda "λ"> <!-- greek small letter lamda,
+ U+03BB ISOgrk3 -->
+<!ENTITY mu "μ"> <!-- greek small letter mu, U+03BC ISOgrk3 -->
+<!ENTITY nu "ν"> <!-- greek small letter nu, U+03BD ISOgrk3 -->
+<!ENTITY xi "ξ"> <!-- greek small letter xi, U+03BE ISOgrk3 -->
+<!ENTITY omicron "ο"> <!-- greek small letter omicron, U+03BF NEW -->
+<!ENTITY pi "π"> <!-- greek small letter pi, U+03C0 ISOgrk3 -->
+<!ENTITY rho "ρ"> <!-- greek small letter rho, U+03C1 ISOgrk3 -->
+<!ENTITY sigmaf "ς"> <!-- greek small letter final sigma,
+ U+03C2 ISOgrk3 -->
+<!ENTITY sigma "σ"> <!-- greek small letter sigma,
+ U+03C3 ISOgrk3 -->
+<!ENTITY tau "τ"> <!-- greek small letter tau, U+03C4 ISOgrk3 -->
+<!ENTITY upsilon "υ"> <!-- greek small letter upsilon,
+ U+03C5 ISOgrk3 -->
+<!ENTITY phi "φ"> <!-- greek small letter phi, U+03C6 ISOgrk3 -->
+<!ENTITY chi "χ"> <!-- greek small letter chi, U+03C7 ISOgrk3 -->
+<!ENTITY psi "ψ"> <!-- greek small letter psi, U+03C8 ISOgrk3 -->
+<!ENTITY omega "ω"> <!-- greek small letter omega,
+ U+03C9 ISOgrk3 -->
+<!ENTITY thetasym "ϑ"> <!-- greek theta symbol,
+ U+03D1 NEW -->
+<!ENTITY upsih "ϒ"> <!-- greek upsilon with hook symbol,
+ U+03D2 NEW -->
+<!ENTITY piv "ϖ"> <!-- greek pi symbol, U+03D6 ISOgrk3 -->
+
+<!-- General Punctuation -->
+<!ENTITY bull "•"> <!-- bullet = black small circle,
+ U+2022 ISOpub -->
+<!-- bullet is NOT the same as bullet operator, U+2219 -->
+<!ENTITY hellip "…"> <!-- horizontal ellipsis = three dot leader,
+ U+2026 ISOpub -->
+<!ENTITY prime "′"> <!-- prime = minutes = feet, U+2032 ISOtech -->
+<!ENTITY Prime "″"> <!-- double prime = seconds = inches,
+ U+2033 ISOtech -->
+<!ENTITY oline "‾"> <!-- overline = spacing overscore,
+ U+203E NEW -->
+<!ENTITY frasl "⁄"> <!-- fraction slash, U+2044 NEW -->
+
+<!-- Letterlike Symbols -->
+<!ENTITY weierp "℘"> <!-- script capital P = power set
+ = Weierstrass p, U+2118 ISOamso -->
+<!ENTITY image "ℑ"> <!-- black-letter capital I = imaginary part,
+ U+2111 ISOamso -->
+<!ENTITY real "ℜ"> <!-- black-letter capital R = real part symbol,
+ U+211C ISOamso -->
+<!ENTITY trade "™"> <!-- trade mark sign, U+2122 ISOnum -->
+<!ENTITY alefsym "ℵ"> <!-- alef symbol = first transfinite cardinal,
+ U+2135 NEW -->
+<!-- alef symbol is NOT the same as hebrew letter alef,
+ U+05D0 although the same glyph could be used to depict both characters -->
+
+<!-- Arrows -->
+<!ENTITY larr "←"> <!-- leftwards arrow, U+2190 ISOnum -->
+<!ENTITY uarr "↑"> <!-- upwards arrow, U+2191 ISOnum-->
+<!ENTITY rarr "→"> <!-- rightwards arrow, U+2192 ISOnum -->
+<!ENTITY darr "↓"> <!-- downwards arrow, U+2193 ISOnum -->
+<!ENTITY harr "↔"> <!-- left right arrow, U+2194 ISOamsa -->
+<!ENTITY crarr "↵"> <!-- downwards arrow with corner leftwards
+ = carriage return, U+21B5 NEW -->
+<!ENTITY lArr "⇐"> <!-- leftwards double arrow, U+21D0 ISOtech -->
+<!-- Unicode does not say that lArr is the same as the 'is implied by' arrow
+ but also does not have any other character for that function. So lArr can
+ be used for 'is implied by' as ISOtech suggests -->
+<!ENTITY uArr "⇑"> <!-- upwards double arrow, U+21D1 ISOamsa -->
+<!ENTITY rArr "⇒"> <!-- rightwards double arrow,
+ U+21D2 ISOtech -->
+<!-- Unicode does not say this is the 'implies' character but does not have
+ another character with this function so rArr can be used for 'implies'
+ as ISOtech suggests -->
+<!ENTITY dArr "⇓"> <!-- downwards double arrow, U+21D3 ISOamsa -->
+<!ENTITY hArr "⇔"> <!-- left right double arrow,
+ U+21D4 ISOamsa -->
+
+<!-- Mathematical Operators -->
+<!ENTITY forall "∀"> <!-- for all, U+2200 ISOtech -->
+<!ENTITY part "∂"> <!-- partial differential, U+2202 ISOtech -->
+<!ENTITY exist "∃"> <!-- there exists, U+2203 ISOtech -->
+<!ENTITY empty "∅"> <!-- empty set = null set, U+2205 ISOamso -->
+<!ENTITY nabla "∇"> <!-- nabla = backward difference,
+ U+2207 ISOtech -->
+<!ENTITY isin "∈"> <!-- element of, U+2208 ISOtech -->
+<!ENTITY notin "∉"> <!-- not an element of, U+2209 ISOtech -->
+<!ENTITY ni "∋"> <!-- contains as member, U+220B ISOtech -->
+<!ENTITY prod "∏"> <!-- n-ary product = product sign,
+ U+220F ISOamsb -->
+<!-- prod is NOT the same character as U+03A0 'greek capital letter pi' though
+ the same glyph might be used for both -->
+<!ENTITY sum "∑"> <!-- n-ary summation, U+2211 ISOamsb -->
+<!-- sum is NOT the same character as U+03A3 'greek capital letter sigma'
+ though the same glyph might be used for both -->
+<!ENTITY minus "−"> <!-- minus sign, U+2212 ISOtech -->
+<!ENTITY lowast "∗"> <!-- asterisk operator, U+2217 ISOtech -->
+<!ENTITY radic "√"> <!-- square root = radical sign,
+ U+221A ISOtech -->
+<!ENTITY prop "∝"> <!-- proportional to, U+221D ISOtech -->
+<!ENTITY infin "∞"> <!-- infinity, U+221E ISOtech -->
+<!ENTITY ang "∠"> <!-- angle, U+2220 ISOamso -->
+<!ENTITY and "∧"> <!-- logical and = wedge, U+2227 ISOtech -->
+<!ENTITY or "∨"> <!-- logical or = vee, U+2228 ISOtech -->
+<!ENTITY cap "∩"> <!-- intersection = cap, U+2229 ISOtech -->
+<!ENTITY cup "∪"> <!-- union = cup, U+222A ISOtech -->
+<!ENTITY int "∫"> <!-- integral, U+222B ISOtech -->
+<!ENTITY there4 "∴"> <!-- therefore, U+2234 ISOtech -->
+<!ENTITY sim "∼"> <!-- tilde operator = varies with = similar to,
+ U+223C ISOtech -->
+<!-- tilde operator is NOT the same character as the tilde, U+007E,
+ although the same glyph might be used to represent both -->
+<!ENTITY cong "≅"> <!-- approximately equal to, U+2245 ISOtech -->
+<!ENTITY asymp "≈"> <!-- almost equal to = asymptotic to,
+ U+2248 ISOamsr -->
+<!ENTITY ne "≠"> <!-- not equal to, U+2260 ISOtech -->
+<!ENTITY equiv "≡"> <!-- identical to, U+2261 ISOtech -->
+<!ENTITY le "≤"> <!-- less-than or equal to, U+2264 ISOtech -->
+<!ENTITY ge "≥"> <!-- greater-than or equal to,
+ U+2265 ISOtech -->
+<!ENTITY sub "⊂"> <!-- subset of, U+2282 ISOtech -->
+<!ENTITY sup "⊃"> <!-- superset of, U+2283 ISOtech -->
+<!ENTITY nsub "⊄"> <!-- not a subset of, U+2284 ISOamsn -->
+<!ENTITY sube "⊆"> <!-- subset of or equal to, U+2286 ISOtech -->
+<!ENTITY supe "⊇"> <!-- superset of or equal to,
+ U+2287 ISOtech -->
+<!ENTITY oplus "⊕"> <!-- circled plus = direct sum,
+ U+2295 ISOamsb -->
+<!ENTITY otimes "⊗"> <!-- circled times = vector product,
+ U+2297 ISOamsb -->
+<!ENTITY perp "⊥"> <!-- up tack = orthogonal to = perpendicular,
+ U+22A5 ISOtech -->
+<!ENTITY sdot "⋅"> <!-- dot operator, U+22C5 ISOamsb -->
+<!-- dot operator is NOT the same character as U+00B7 middle dot -->
+
+<!-- Miscellaneous Technical -->
+<!ENTITY lceil "⌈"> <!-- left ceiling = APL upstile,
+ U+2308 ISOamsc -->
+<!ENTITY rceil "⌉"> <!-- right ceiling, U+2309 ISOamsc -->
+<!ENTITY lfloor "⌊"> <!-- left floor = APL downstile,
+ U+230A ISOamsc -->
+<!ENTITY rfloor "⌋"> <!-- right floor, U+230B ISOamsc -->
+<!ENTITY lang "〈"> <!-- left-pointing angle bracket = bra,
+ U+2329 ISOtech -->
+<!-- lang is NOT the same character as U+003C 'less than sign'
+ or U+2039 'single left-pointing angle quotation mark' -->
+<!ENTITY rang "〉"> <!-- right-pointing angle bracket = ket,
+ U+232A ISOtech -->
+<!-- rang is NOT the same character as U+003E 'greater than sign'
+ or U+203A 'single right-pointing angle quotation mark' -->
+
+<!-- Geometric Shapes -->
+<!ENTITY loz "◊"> <!-- lozenge, U+25CA ISOpub -->
+
+<!-- Miscellaneous Symbols -->
+<!ENTITY spades "♠"> <!-- black spade suit, U+2660 ISOpub -->
+<!-- black here seems to mean filled as opposed to hollow -->
+<!ENTITY clubs "♣"> <!-- black club suit = shamrock,
+ U+2663 ISOpub -->
+<!ENTITY hearts "♥"> <!-- black heart suit = valentine,
+ U+2665 ISOpub -->
+<!ENTITY diams "♦"> <!-- black diamond suit, U+2666 ISOpub -->
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dtd/xhtml1-frameset.dtd Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,1235 @@
+<!--
+ Extensible HTML version 1.0 Frameset DTD
+
+ This is the same as HTML 4 Frameset except for
+ changes due to the differences between XML and SGML.
+
+ Namespace = http://www.w3.org/1999/xhtml
+
+ For further information, see: http://www.w3.org/TR/xhtml1
+
+ Copyright (c) 1998-2002 W3C (MIT, INRIA, Keio),
+ All Rights Reserved.
+
+ This DTD module is identified by the PUBLIC and SYSTEM identifiers:
+
+ PUBLIC "-//W3C//DTD XHTML 1.0 Frameset//EN"
+ SYSTEM "http://www.w3.org/TR/xhtml1/DTD/xhtml1-frameset.dtd"
+
+ $Revision$
+ $Date$
+
+-->
+
+<!--================ Character mnemonic entities =========================-->
+
+<!ENTITY % HTMLlat1 PUBLIC
+ "-//W3C//ENTITIES Latin 1 for XHTML//EN"
+ "xhtml-lat1.ent">
+%HTMLlat1;
+
+<!ENTITY % HTMLsymbol PUBLIC
+ "-//W3C//ENTITIES Symbols for XHTML//EN"
+ "xhtml-symbol.ent">
+%HTMLsymbol;
+
+<!ENTITY % HTMLspecial PUBLIC
+ "-//W3C//ENTITIES Special for XHTML//EN"
+ "xhtml-special.ent">
+%HTMLspecial;
+
+<!--================== Imported Names ====================================-->
+
+<!ENTITY % ContentType "CDATA">
+ <!-- media type, as per [RFC2045] -->
+
+<!ENTITY % ContentTypes "CDATA">
+ <!-- comma-separated list of media types, as per [RFC2045] -->
+
+<!ENTITY % Charset "CDATA">
+ <!-- a character encoding, as per [RFC2045] -->
+
+<!ENTITY % Charsets "CDATA">
+ <!-- a space separated list of character encodings, as per [RFC2045] -->
+
+<!ENTITY % LanguageCode "NMTOKEN">
+ <!-- a language code, as per [RFC3066] -->
+
+<!ENTITY % Character "CDATA">
+ <!-- a single character, as per section 2.2 of [XML] -->
+
+<!ENTITY % Number "CDATA">
+ <!-- one or more digits -->
+
+<!ENTITY % LinkTypes "CDATA">
+ <!-- space-separated list of link types -->
+
+<!ENTITY % MediaDesc "CDATA">
+ <!-- single or comma-separated list of media descriptors -->
+
+<!ENTITY % URI "CDATA">
+ <!-- a Uniform Resource Identifier, see [RFC2396] -->
+
+<!ENTITY % UriList "CDATA">
+ <!-- a space separated list of Uniform Resource Identifiers -->
+
+<!ENTITY % Datetime "CDATA">
+ <!-- date and time information. ISO date format -->
+
+<!ENTITY % Script "CDATA">
+ <!-- script expression -->
+
+<!ENTITY % StyleSheet "CDATA">
+ <!-- style sheet data -->
+
+<!ENTITY % Text "CDATA">
+ <!-- used for titles etc. -->
+
+<!ENTITY % FrameTarget "NMTOKEN">
+ <!-- render in this frame -->
+
+<!ENTITY % Length "CDATA">
+ <!-- nn for pixels or nn% for percentage length -->
+
+<!ENTITY % MultiLength "CDATA">
+ <!-- pixel, percentage, or relative -->
+
+<!ENTITY % MultiLengths "CDATA">
+ <!-- comma-separated list of MultiLength -->
+
+<!ENTITY % Pixels "CDATA">
+ <!-- integer representing length in pixels -->
+
+<!-- these are used for image maps -->
+
+<!ENTITY % Shape "(rect|circle|poly|default)">
+
+<!ENTITY % Coords "CDATA">
+ <!-- comma separated list of lengths -->
+
+<!-- used for object, applet, img, input and iframe -->
+<!ENTITY % ImgAlign "(top|middle|bottom|left|right)">
+
+<!-- a color using sRGB: #RRGGBB as Hex values -->
+<!ENTITY % Color "CDATA">
+
+<!-- There are also 16 widely known color names with their sRGB values:
+
+ Black = #000000 Green = #008000
+ Silver = #C0C0C0 Lime = #00FF00
+ Gray = #808080 Olive = #808000
+ White = #FFFFFF Yellow = #FFFF00
+ Maroon = #800000 Navy = #000080
+ Red = #FF0000 Blue = #0000FF
+ Purple = #800080 Teal = #008080
+ Fuchsia= #FF00FF Aqua = #00FFFF
+-->
+
+<!--=================== Generic Attributes ===============================-->
+
+<!-- core attributes common to most elements
+ id document-wide unique id
+ class space separated list of classes
+ style associated style info
+ title advisory title/amplification
+-->
+<!ENTITY % coreattrs
+ "id ID #IMPLIED
+ class CDATA #IMPLIED
+ style %StyleSheet; #IMPLIED
+ title %Text; #IMPLIED"
+ >
+
+<!-- internationalization attributes
+ lang language code (backwards compatible)
+ xml:lang language code (as per XML 1.0 spec)
+ dir direction for weak/neutral text
+-->
+<!ENTITY % i18n
+ "lang %LanguageCode; #IMPLIED
+ xml:lang %LanguageCode; #IMPLIED
+ dir (ltr|rtl) #IMPLIED"
+ >
+
+<!-- attributes for common UI events
+ onclick a pointer button was clicked
+ ondblclick a pointer button was double clicked
+ onmousedown a pointer button was pressed down
+ onmouseup a pointer button was released
+ onmousemove a pointer was moved onto the element
+ onmouseout a pointer was moved away from the element
+ onkeypress a key was pressed and released
+ onkeydown a key was pressed down
+ onkeyup a key was released
+-->
+<!ENTITY % events
+ "onclick %Script; #IMPLIED
+ ondblclick %Script; #IMPLIED
+ onmousedown %Script; #IMPLIED
+ onmouseup %Script; #IMPLIED
+ onmouseover %Script; #IMPLIED
+ onmousemove %Script; #IMPLIED
+ onmouseout %Script; #IMPLIED
+ onkeypress %Script; #IMPLIED
+ onkeydown %Script; #IMPLIED
+ onkeyup %Script; #IMPLIED"
+ >
+
+<!-- attributes for elements that can get the focus
+ accesskey accessibility key character
+ tabindex position in tabbing order
+ onfocus the element got the focus
+ onblur the element lost the focus
+-->
+<!ENTITY % focus
+ "accesskey %Character; #IMPLIED
+ tabindex %Number; #IMPLIED
+ onfocus %Script; #IMPLIED
+ onblur %Script; #IMPLIED"
+ >
+
+<!ENTITY % attrs "%coreattrs; %i18n; %events;">
+
+<!-- text alignment for p, div, h1-h6. The default is
+ align="left" for ltr headings, "right" for rtl -->
+
+<!ENTITY % TextAlign "align (left|center|right|justify) #IMPLIED">
+
+<!--=================== Text Elements ====================================-->
+
+<!ENTITY % special.extra
+ "object | applet | img | map | iframe">
+
+<!ENTITY % special.basic
+ "br | span | bdo">
+
+<!ENTITY % special
+ "%special.basic; | %special.extra;">
+
+<!ENTITY % fontstyle.extra "big | small | font | basefont">
+
+<!ENTITY % fontstyle.basic "tt | i | b | u
+ | s | strike ">
+
+<!ENTITY % fontstyle "%fontstyle.basic; | %fontstyle.extra;">
+
+<!ENTITY % phrase.extra "sub | sup">
+<!ENTITY % phrase.basic "em | strong | dfn | code | q |
+ samp | kbd | var | cite | abbr | acronym">
+
+<!ENTITY % phrase "%phrase.basic; | %phrase.extra;">
+
+<!ENTITY % inline.forms "input | select | textarea | label | button">
+
+<!-- these can occur at block or inline level -->
+<!ENTITY % misc.inline "ins | del | script">
+
+<!-- these can only occur at block level -->
+<!ENTITY % misc "noscript | %misc.inline;">
+
+
+<!ENTITY % inline "a | %special; | %fontstyle; | %phrase; | %inline.forms;">
+
+<!-- %Inline; covers inline or "text-level" elements -->
+<!ENTITY % Inline "(#PCDATA | %inline; | %misc.inline;)*">
+
+<!--================== Block level elements ==============================-->
+
+<!ENTITY % heading "h1|h2|h3|h4|h5|h6">
+<!ENTITY % lists "ul | ol | dl | menu | dir">
+<!ENTITY % blocktext "pre | hr | blockquote | address | center">
+
+<!ENTITY % block
+ "p | %heading; | div | %lists; | %blocktext; | isindex | fieldset | table">
+
+<!-- %Flow; mixes block and inline and is used for list items etc. -->
+<!ENTITY % Flow "(#PCDATA | %block; | form | %inline; | %misc;)*">
+
+<!--================== Content models for exclusions =====================-->
+
+<!-- a elements use %Inline; excluding a -->
+
+<!ENTITY % a.content
+ "(#PCDATA | %special; | %fontstyle; | %phrase; | %inline.forms; | %misc.inline;)*">
+
+<!-- pre uses %Inline excluding img, object, applet, big, small,
+ sub, sup, font, or basefont -->
+
+<!ENTITY % pre.content
+ "(#PCDATA | a | %special.basic; | %fontstyle.basic; | %phrase.basic; |
+ %inline.forms; | %misc.inline;)*">
+
+
+<!-- form uses %Flow; excluding form -->
+
+<!ENTITY % form.content "(#PCDATA | %block; | %inline; | %misc;)*">
+
+<!-- button uses %Flow; but excludes a, form, form controls, iframe -->
+
+<!ENTITY % button.content
+ "(#PCDATA | p | %heading; | div | %lists; | %blocktext; |
+ table | br | span | bdo | object | applet | img | map |
+ %fontstyle; | %phrase; | %misc;)*">
+
+<!--================ Document Structure ==================================-->
+
+<!-- the namespace URI designates the document profile -->
+
+<!ELEMENT html (head, frameset)>
+<!ATTLIST html
+ %i18n;
+ id ID #IMPLIED
+ xmlns %URI; #FIXED 'http://www.w3.org/1999/xhtml'
+ >
+
+<!--================ Document Head =======================================-->
+
+<!ENTITY % head.misc "(script|style|meta|link|object|isindex)*">
+
+<!-- content model is %head.misc; combined with a single
+ title and an optional base element in any order -->
+
+<!ELEMENT head (%head.misc;,
+ ((title, %head.misc;, (base, %head.misc;)?) |
+ (base, %head.misc;, (title, %head.misc;))))>
+
+<!ATTLIST head
+ %i18n;
+ id ID #IMPLIED
+ profile %URI; #IMPLIED
+ >
+
+<!-- The title element is not considered part of the flow of text.
+ It should be displayed, for example as the page header or
+ window title. Exactly one title is required per document.
+ -->
+<!ELEMENT title (#PCDATA)>
+<!ATTLIST title
+ %i18n;
+ id ID #IMPLIED
+ >
+
+<!-- document base URI -->
+
+<!ELEMENT base EMPTY>
+<!ATTLIST base
+ id ID #IMPLIED
+ href %URI; #IMPLIED
+ target %FrameTarget; #IMPLIED
+ >
+
+<!-- generic metainformation -->
+<!ELEMENT meta EMPTY>
+<!ATTLIST meta
+ %i18n;
+ id ID #IMPLIED
+ http-equiv CDATA #IMPLIED
+ name CDATA #IMPLIED
+ content CDATA #REQUIRED
+ scheme CDATA #IMPLIED
+ >
+
+<!--
+ Relationship values can be used in principle:
+
+ a) for document specific toolbars/menus when used
+ with the link element in document head e.g.
+ start, contents, previous, next, index, end, help
+ b) to link to a separate style sheet (rel="stylesheet")
+ c) to make a link to a script (rel="script")
+ d) by stylesheets to control how collections of
+ html nodes are rendered into printed documents
+ e) to make a link to a printable version of this document
+ e.g. a PostScript or PDF version (rel="alternate" media="print")
+-->
+
+<!ELEMENT link EMPTY>
+<!ATTLIST link
+ %attrs;
+ charset %Charset; #IMPLIED
+ href %URI; #IMPLIED
+ hreflang %LanguageCode; #IMPLIED
+ type %ContentType; #IMPLIED
+ rel %LinkTypes; #IMPLIED
+ rev %LinkTypes; #IMPLIED
+ media %MediaDesc; #IMPLIED
+ target %FrameTarget; #IMPLIED
+ >
+
+<!-- style info, which may include CDATA sections -->
+<!ELEMENT style (#PCDATA)>
+<!ATTLIST style
+ %i18n;
+ id ID #IMPLIED
+ type %ContentType; #REQUIRED
+ media %MediaDesc; #IMPLIED
+ title %Text; #IMPLIED
+ xml:space (preserve) #FIXED 'preserve'
+ >
+
+<!-- script statements, which may include CDATA sections -->
+<!ELEMENT script (#PCDATA)>
+<!ATTLIST script
+ id ID #IMPLIED
+ charset %Charset; #IMPLIED
+ type %ContentType; #REQUIRED
+ language CDATA #IMPLIED
+ src %URI; #IMPLIED
+ defer (defer) #IMPLIED
+ xml:space (preserve) #FIXED 'preserve'
+ >
+
+<!-- alternate content container for non script-based rendering -->
+
+<!ELEMENT noscript %Flow;>
+<!ATTLIST noscript
+ %attrs;
+ >
+
+<!--======================= Frames =======================================-->
+
+<!-- only one noframes element permitted per document -->
+
+<!ELEMENT frameset (frameset|frame|noframes)*>
+<!ATTLIST frameset
+ %coreattrs;
+ rows %MultiLengths; #IMPLIED
+ cols %MultiLengths; #IMPLIED
+ onload %Script; #IMPLIED
+ onunload %Script; #IMPLIED
+ >
+
+<!-- reserved frame names start with "_" otherwise starts with letter -->
+
+<!-- tiled window within frameset -->
+
+<!ELEMENT frame EMPTY>
+<!ATTLIST frame
+ %coreattrs;
+ longdesc %URI; #IMPLIED
+ name NMTOKEN #IMPLIED
+ src %URI; #IMPLIED
+ frameborder (1|0) "1"
+ marginwidth %Pixels; #IMPLIED
+ marginheight %Pixels; #IMPLIED
+ noresize (noresize) #IMPLIED
+ scrolling (yes|no|auto) "auto"
+ >
+
+<!-- inline subwindow -->
+
+<!ELEMENT iframe %Flow;>
+<!ATTLIST iframe
+ %coreattrs;
+ longdesc %URI; #IMPLIED
+ name NMTOKEN #IMPLIED
+ src %URI; #IMPLIED
+ frameborder (1|0) "1"
+ marginwidth %Pixels; #IMPLIED
+ marginheight %Pixels; #IMPLIED
+ scrolling (yes|no|auto) "auto"
+ align %ImgAlign; #IMPLIED
+ height %Length; #IMPLIED
+ width %Length; #IMPLIED
+ >
+
+<!-- alternate content container for non frame-based rendering -->
+
+<!ELEMENT noframes (body)>
+<!ATTLIST noframes
+ %attrs;
+ >
+
+<!--=================== Document Body ====================================-->
+
+<!ELEMENT body %Flow;>
+<!ATTLIST body
+ %attrs;
+ onload %Script; #IMPLIED
+ onunload %Script; #IMPLIED
+ background %URI; #IMPLIED
+ bgcolor %Color; #IMPLIED
+ text %Color; #IMPLIED
+ link %Color; #IMPLIED
+ vlink %Color; #IMPLIED
+ alink %Color; #IMPLIED
+ >
+
+<!ELEMENT div %Flow;> <!-- generic language/style container -->
+<!ATTLIST div
+ %attrs;
+ %TextAlign;
+ >
+
+<!--=================== Paragraphs =======================================-->
+
+<!ELEMENT p %Inline;>
+<!ATTLIST p
+ %attrs;
+ %TextAlign;
+ >
+
+<!--=================== Headings =========================================-->
+
+<!--
+ There are six levels of headings from h1 (the most important)
+ to h6 (the least important).
+-->
+
+<!ELEMENT h1 %Inline;>
+<!ATTLIST h1
+ %attrs;
+ %TextAlign;
+ >
+
+<!ELEMENT h2 %Inline;>
+<!ATTLIST h2
+ %attrs;
+ %TextAlign;
+ >
+
+<!ELEMENT h3 %Inline;>
+<!ATTLIST h3
+ %attrs;
+ %TextAlign;
+ >
+
+<!ELEMENT h4 %Inline;>
+<!ATTLIST h4
+ %attrs;
+ %TextAlign;
+ >
+
+<!ELEMENT h5 %Inline;>
+<!ATTLIST h5
+ %attrs;
+ %TextAlign;
+ >
+
+<!ELEMENT h6 %Inline;>
+<!ATTLIST h6
+ %attrs;
+ %TextAlign;
+ >
+
+<!--=================== Lists ============================================-->
+
+<!-- Unordered list bullet styles -->
+
+<!ENTITY % ULStyle "(disc|square|circle)">
+
+<!-- Unordered list -->
+
+<!ELEMENT ul (li)+>
+<!ATTLIST ul
+ %attrs;
+ type %ULStyle; #IMPLIED
+ compact (compact) #IMPLIED
+ >
+
+<!-- Ordered list numbering style
+
+ 1 arabic numbers 1, 2, 3, ...
+ a lower alpha a, b, c, ...
+ A upper alpha A, B, C, ...
+ i lower roman i, ii, iii, ...
+ I upper roman I, II, III, ...
+
+ The style is applied to the sequence number which by default
+ is reset to 1 for the first list item in an ordered list.
+-->
+<!ENTITY % OLStyle "CDATA">
+
+<!-- Ordered (numbered) list -->
+
+<!ELEMENT ol (li)+>
+<!ATTLIST ol
+ %attrs;
+ type %OLStyle; #IMPLIED
+ compact (compact) #IMPLIED
+ start %Number; #IMPLIED
+ >
+
+<!-- single column list (DEPRECATED) -->
+<!ELEMENT menu (li)+>
+<!ATTLIST menu
+ %attrs;
+ compact (compact) #IMPLIED
+ >
+
+<!-- multiple column list (DEPRECATED) -->
+<!ELEMENT dir (li)+>
+<!ATTLIST dir
+ %attrs;
+ compact (compact) #IMPLIED
+ >
+
+<!-- LIStyle is constrained to: "(%ULStyle;|%OLStyle;)" -->
+<!ENTITY % LIStyle "CDATA">
+
+<!-- list item -->
+
+<!ELEMENT li %Flow;>
+<!ATTLIST li
+ %attrs;
+ type %LIStyle; #IMPLIED
+ value %Number; #IMPLIED
+ >
+
+<!-- definition lists - dt for term, dd for its definition -->
+
+<!ELEMENT dl (dt|dd)+>
+<!ATTLIST dl
+ %attrs;
+ compact (compact) #IMPLIED
+ >
+
+<!ELEMENT dt %Inline;>
+<!ATTLIST dt
+ %attrs;
+ >
+
+<!ELEMENT dd %Flow;>
+<!ATTLIST dd
+ %attrs;
+ >
+
+<!--=================== Address ==========================================-->
+
+<!-- information on author -->
+
+<!ELEMENT address (#PCDATA | %inline; | %misc.inline; | p)*>
+<!ATTLIST address
+ %attrs;
+ >
+
+<!--=================== Horizontal Rule ==================================-->
+
+<!ELEMENT hr EMPTY>
+<!ATTLIST hr
+ %attrs;
+ align (left|center|right) #IMPLIED
+ noshade (noshade) #IMPLIED
+ size %Pixels; #IMPLIED
+ width %Length; #IMPLIED
+ >
+
+<!--=================== Preformatted Text ================================-->
+
+<!-- content is %Inline; excluding
+ "img|object|applet|big|small|sub|sup|font|basefont" -->
+
+<!ELEMENT pre %pre.content;>
+<!ATTLIST pre
+ %attrs;
+ width %Number; #IMPLIED
+ xml:space (preserve) #FIXED 'preserve'
+ >
+
+<!--=================== Block-like Quotes ================================-->
+
+<!ELEMENT blockquote %Flow;>
+<!ATTLIST blockquote
+ %attrs;
+ cite %URI; #IMPLIED
+ >
+
+<!--=================== Text alignment ===================================-->
+
+<!-- center content -->
+<!ELEMENT center %Flow;>
+<!ATTLIST center
+ %attrs;
+ >
+
+<!--=================== Inserted/Deleted Text ============================-->
+
+
+<!--
+ ins/del are allowed in block and inline content, but its
+ inappropriate to include block content within an ins element
+ occurring in inline content.
+-->
+<!ELEMENT ins %Flow;>
+<!ATTLIST ins
+ %attrs;
+ cite %URI; #IMPLIED
+ datetime %Datetime; #IMPLIED
+ >
+
+<!ELEMENT del %Flow;>
+<!ATTLIST del
+ %attrs;
+ cite %URI; #IMPLIED
+ datetime %Datetime; #IMPLIED
+ >
+
+<!--================== The Anchor Element ================================-->
+
+<!-- content is %Inline; except that anchors shouldn't be nested -->
+
+<!ELEMENT a %a.content;>
+<!ATTLIST a
+ %attrs;
+ %focus;
+ charset %Charset; #IMPLIED
+ type %ContentType; #IMPLIED
+ name NMTOKEN #IMPLIED
+ href %URI; #IMPLIED
+ hreflang %LanguageCode; #IMPLIED
+ rel %LinkTypes; #IMPLIED
+ rev %LinkTypes; #IMPLIED
+ shape %Shape; "rect"
+ coords %Coords; #IMPLIED
+ target %FrameTarget; #IMPLIED
+ >
+
+<!--===================== Inline Elements ================================-->
+
+<!ELEMENT span %Inline;> <!-- generic language/style container -->
+<!ATTLIST span
+ %attrs;
+ >
+
+<!ELEMENT bdo %Inline;> <!-- I18N BiDi over-ride -->
+<!ATTLIST bdo
+ %coreattrs;
+ %events;
+ lang %LanguageCode; #IMPLIED
+ xml:lang %LanguageCode; #IMPLIED
+ dir (ltr|rtl) #REQUIRED
+ >
+
+<!ELEMENT br EMPTY> <!-- forced line break -->
+<!ATTLIST br
+ %coreattrs;
+ clear (left|all|right|none) "none"
+ >
+
+<!ELEMENT em %Inline;> <!-- emphasis -->
+<!ATTLIST em %attrs;>
+
+<!ELEMENT strong %Inline;> <!-- strong emphasis -->
+<!ATTLIST strong %attrs;>
+
+<!ELEMENT dfn %Inline;> <!-- definitional -->
+<!ATTLIST dfn %attrs;>
+
+<!ELEMENT code %Inline;> <!-- program code -->
+<!ATTLIST code %attrs;>
+
+<!ELEMENT samp %Inline;> <!-- sample -->
+<!ATTLIST samp %attrs;>
+
+<!ELEMENT kbd %Inline;> <!-- something user would type -->
+<!ATTLIST kbd %attrs;>
+
+<!ELEMENT var %Inline;> <!-- variable -->
+<!ATTLIST var %attrs;>
+
+<!ELEMENT cite %Inline;> <!-- citation -->
+<!ATTLIST cite %attrs;>
+
+<!ELEMENT abbr %Inline;> <!-- abbreviation -->
+<!ATTLIST abbr %attrs;>
+
+<!ELEMENT acronym %Inline;> <!-- acronym -->
+<!ATTLIST acronym %attrs;>
+
+<!ELEMENT q %Inline;> <!-- inlined quote -->
+<!ATTLIST q
+ %attrs;
+ cite %URI; #IMPLIED
+ >
+
+<!ELEMENT sub %Inline;> <!-- subscript -->
+<!ATTLIST sub %attrs;>
+
+<!ELEMENT sup %Inline;> <!-- superscript -->
+<!ATTLIST sup %attrs;>
+
+<!ELEMENT tt %Inline;> <!-- fixed pitch font -->
+<!ATTLIST tt %attrs;>
+
+<!ELEMENT i %Inline;> <!-- italic font -->
+<!ATTLIST i %attrs;>
+
+<!ELEMENT b %Inline;> <!-- bold font -->
+<!ATTLIST b %attrs;>
+
+<!ELEMENT big %Inline;> <!-- bigger font -->
+<!ATTLIST big %attrs;>
+
+<!ELEMENT small %Inline;> <!-- smaller font -->
+<!ATTLIST small %attrs;>
+
+<!ELEMENT u %Inline;> <!-- underline -->
+<!ATTLIST u %attrs;>
+
+<!ELEMENT s %Inline;> <!-- strike-through -->
+<!ATTLIST s %attrs;>
+
+<!ELEMENT strike %Inline;> <!-- strike-through -->
+<!ATTLIST strike %attrs;>
+
+<!ELEMENT basefont EMPTY> <!-- base font size -->
+<!ATTLIST basefont
+ id ID #IMPLIED
+ size CDATA #REQUIRED
+ color %Color; #IMPLIED
+ face CDATA #IMPLIED
+ >
+
+<!ELEMENT font %Inline;> <!-- local change to font -->
+<!ATTLIST font
+ %coreattrs;
+ %i18n;
+ size CDATA #IMPLIED
+ color %Color; #IMPLIED
+ face CDATA #IMPLIED
+ >
+
+<!--==================== Object ======================================-->
+<!--
+ object is used to embed objects as part of HTML pages.
+ param elements should precede other content. Parameters
+ can also be expressed as attribute/value pairs on the
+ object element itself when brevity is desired.
+-->
+
+<!ELEMENT object (#PCDATA | param | %block; | form |%inline; | %misc;)*>
+<!ATTLIST object
+ %attrs;
+ declare (declare) #IMPLIED
+ classid %URI; #IMPLIED
+ codebase %URI; #IMPLIED
+ data %URI; #IMPLIED
+ type %ContentType; #IMPLIED
+ codetype %ContentType; #IMPLIED
+ archive %UriList; #IMPLIED
+ standby %Text; #IMPLIED
+ height %Length; #IMPLIED
+ width %Length; #IMPLIED
+ usemap %URI; #IMPLIED
+ name NMTOKEN #IMPLIED
+ tabindex %Number; #IMPLIED
+ align %ImgAlign; #IMPLIED
+ border %Pixels; #IMPLIED
+ hspace %Pixels; #IMPLIED
+ vspace %Pixels; #IMPLIED
+ >
+
+<!--
+ param is used to supply a named property value.
+ In XML it would seem natural to follow RDF and support an
+ abbreviated syntax where the param elements are replaced
+ by attribute value pairs on the object start tag.
+-->
+<!ELEMENT param EMPTY>
+<!ATTLIST param
+ id ID #IMPLIED
+ name CDATA #REQUIRED
+ value CDATA #IMPLIED
+ valuetype (data|ref|object) "data"
+ type %ContentType; #IMPLIED
+ >
+
+<!--=================== Java applet ==================================-->
+<!--
+ One of code or object attributes must be present.
+ Place param elements before other content.
+-->
+<!ELEMENT applet (#PCDATA | param | %block; | form | %inline; | %misc;)*>
+<!ATTLIST applet
+ %coreattrs;
+ codebase %URI; #IMPLIED
+ archive CDATA #IMPLIED
+ code CDATA #IMPLIED
+ object CDATA #IMPLIED
+ alt %Text; #IMPLIED
+ name NMTOKEN #IMPLIED
+ width %Length; #REQUIRED
+ height %Length; #REQUIRED
+ align %ImgAlign; #IMPLIED
+ hspace %Pixels; #IMPLIED
+ vspace %Pixels; #IMPLIED
+ >
+
+<!--=================== Images ===========================================-->
+
+<!--
+ To avoid accessibility problems for people who aren't
+ able to see the image, you should provide a text
+ description using the alt and longdesc attributes.
+ In addition, avoid the use of server-side image maps.
+-->
+
+<!ELEMENT img EMPTY>
+<!ATTLIST img
+ %attrs;
+ src %URI; #REQUIRED
+ alt %Text; #REQUIRED
+ name NMTOKEN #IMPLIED
+ longdesc %URI; #IMPLIED
+ height %Length; #IMPLIED
+ width %Length; #IMPLIED
+ usemap %URI; #IMPLIED
+ ismap (ismap) #IMPLIED
+ align %ImgAlign; #IMPLIED
+ border %Pixels; #IMPLIED
+ hspace %Pixels; #IMPLIED
+ vspace %Pixels; #IMPLIED
+ >
+
+<!-- usemap points to a map element which may be in this document
+ or an external document, although the latter is not widely supported -->
+
+<!--================== Client-side image maps ============================-->
+
+<!-- These can be placed in the same document or grouped in a
+ separate document although this isn't yet widely supported -->
+
+<!ELEMENT map ((%block; | form | %misc;)+ | area+)>
+<!ATTLIST map
+ %i18n;
+ %events;
+ id ID #REQUIRED
+ class CDATA #IMPLIED
+ style %StyleSheet; #IMPLIED
+ title %Text; #IMPLIED
+ name NMTOKEN #IMPLIED
+ >
+
+<!ELEMENT area EMPTY>
+<!ATTLIST area
+ %attrs;
+ %focus;
+ shape %Shape; "rect"
+ coords %Coords; #IMPLIED
+ href %URI; #IMPLIED
+ nohref (nohref) #IMPLIED
+ alt %Text; #REQUIRED
+ target %FrameTarget; #IMPLIED
+ >
+
+<!--================ Forms ===============================================-->
+
+<!ELEMENT form %form.content;> <!-- forms shouldn't be nested -->
+
+<!ATTLIST form
+ %attrs;
+ action %URI; #REQUIRED
+ method (get|post) "get"
+ name NMTOKEN #IMPLIED
+ enctype %ContentType; "application/x-www-form-urlencoded"
+ onsubmit %Script; #IMPLIED
+ onreset %Script; #IMPLIED
+ accept %ContentTypes; #IMPLIED
+ accept-charset %Charsets; #IMPLIED
+ target %FrameTarget; #IMPLIED
+ >
+
+<!--
+ Each label must not contain more than ONE field
+ Label elements shouldn't be nested.
+-->
+<!ELEMENT label %Inline;>
+<!ATTLIST label
+ %attrs;
+ for IDREF #IMPLIED
+ accesskey %Character; #IMPLIED
+ onfocus %Script; #IMPLIED
+ onblur %Script; #IMPLIED
+ >
+
+<!ENTITY % InputType
+ "(text | password | checkbox |
+ radio | submit | reset |
+ file | hidden | image | button)"
+ >
+
+<!-- the name attribute is required for all but submit & reset -->
+
+<!ELEMENT input EMPTY> <!-- form control -->
+<!ATTLIST input
+ %attrs;
+ %focus;
+ type %InputType; "text"
+ name CDATA #IMPLIED
+ value CDATA #IMPLIED
+ checked (checked) #IMPLIED
+ disabled (disabled) #IMPLIED
+ readonly (readonly) #IMPLIED
+ size CDATA #IMPLIED
+ maxlength %Number; #IMPLIED
+ src %URI; #IMPLIED
+ alt CDATA #IMPLIED
+ usemap %URI; #IMPLIED
+ onselect %Script; #IMPLIED
+ onchange %Script; #IMPLIED
+ accept %ContentTypes; #IMPLIED
+ align %ImgAlign; #IMPLIED
+ >
+
+<!ELEMENT select (optgroup|option)+> <!-- option selector -->
+<!ATTLIST select
+ %attrs;
+ name CDATA #IMPLIED
+ size %Number; #IMPLIED
+ multiple (multiple) #IMPLIED
+ disabled (disabled) #IMPLIED
+ tabindex %Number; #IMPLIED
+ onfocus %Script; #IMPLIED
+ onblur %Script; #IMPLIED
+ onchange %Script; #IMPLIED
+ >
+
+<!ELEMENT optgroup (option)+> <!-- option group -->
+<!ATTLIST optgroup
+ %attrs;
+ disabled (disabled) #IMPLIED
+ label %Text; #REQUIRED
+ >
+
+<!ELEMENT option (#PCDATA)> <!-- selectable choice -->
+<!ATTLIST option
+ %attrs;
+ selected (selected) #IMPLIED
+ disabled (disabled) #IMPLIED
+ label %Text; #IMPLIED
+ value CDATA #IMPLIED
+ >
+
+<!ELEMENT textarea (#PCDATA)> <!-- multi-line text field -->
+<!ATTLIST textarea
+ %attrs;
+ %focus;
+ name CDATA #IMPLIED
+ rows %Number; #REQUIRED
+ cols %Number; #REQUIRED
+ disabled (disabled) #IMPLIED
+ readonly (readonly) #IMPLIED
+ onselect %Script; #IMPLIED
+ onchange %Script; #IMPLIED
+ >
+
+<!--
+ The fieldset element is used to group form fields.
+ Only one legend element should occur in the content
+ and if present should only be preceded by whitespace.
+-->
+<!ELEMENT fieldset (#PCDATA | legend | %block; | form | %inline; | %misc;)*>
+<!ATTLIST fieldset
+ %attrs;
+ >
+
+<!ENTITY % LAlign "(top|bottom|left|right)">
+
+<!ELEMENT legend %Inline;> <!-- fieldset label -->
+<!ATTLIST legend
+ %attrs;
+ accesskey %Character; #IMPLIED
+ align %LAlign; #IMPLIED
+ >
+
+<!--
+ Content is %Flow; excluding a, form, form controls, iframe
+-->
+<!ELEMENT button %button.content;> <!-- push button -->
+<!ATTLIST button
+ %attrs;
+ %focus;
+ name CDATA #IMPLIED
+ value CDATA #IMPLIED
+ type (button|submit|reset) "submit"
+ disabled (disabled) #IMPLIED
+ >
+
+<!-- single-line text input control (DEPRECATED) -->
+<!ELEMENT isindex EMPTY>
+<!ATTLIST isindex
+ %coreattrs;
+ %i18n;
+ prompt %Text; #IMPLIED
+ >
+
+<!--======================= Tables =======================================-->
+
+<!-- Derived from IETF HTML table standard, see [RFC1942] -->
+
+<!--
+ The border attribute sets the thickness of the frame around the
+ table. The default units are screen pixels.
+
+ The frame attribute specifies which parts of the frame around
+ the table should be rendered. The values are not the same as
+ CALS to avoid a name clash with the valign attribute.
+-->
+<!ENTITY % TFrame "(void|above|below|hsides|lhs|rhs|vsides|box|border)">
+
+<!--
+ The rules attribute defines which rules to draw between cells:
+
+ If rules is absent then assume:
+ "none" if border is absent or border="0" otherwise "all"
+-->
+
+<!ENTITY % TRules "(none | groups | rows | cols | all)">
+
+<!-- horizontal placement of table relative to document -->
+<!ENTITY % TAlign "(left|center|right)">
+
+<!-- horizontal alignment attributes for cell contents
+
+ char alignment char, e.g. char=":"
+ charoff offset for alignment char
+-->
+<!ENTITY % cellhalign
+ "align (left|center|right|justify|char) #IMPLIED
+ char %Character; #IMPLIED
+ charoff %Length; #IMPLIED"
+ >
+
+<!-- vertical alignment attributes for cell contents -->
+<!ENTITY % cellvalign
+ "valign (top|middle|bottom|baseline) #IMPLIED"
+ >
+
+<!ELEMENT table
+ (caption?, (col*|colgroup*), thead?, tfoot?, (tbody+|tr+))>
+<!ELEMENT caption %Inline;>
+<!ELEMENT thead (tr)+>
+<!ELEMENT tfoot (tr)+>
+<!ELEMENT tbody (tr)+>
+<!ELEMENT colgroup (col)*>
+<!ELEMENT col EMPTY>
+<!ELEMENT tr (th|td)+>
+<!ELEMENT th %Flow;>
+<!ELEMENT td %Flow;>
+
+<!ATTLIST table
+ %attrs;
+ summary %Text; #IMPLIED
+ width %Length; #IMPLIED
+ border %Pixels; #IMPLIED
+ frame %TFrame; #IMPLIED
+ rules %TRules; #IMPLIED
+ cellspacing %Length; #IMPLIED
+ cellpadding %Length; #IMPLIED
+ align %TAlign; #IMPLIED
+ bgcolor %Color; #IMPLIED
+ >
+
+<!ENTITY % CAlign "(top|bottom|left|right)">
+
+<!ATTLIST caption
+ %attrs;
+ align %CAlign; #IMPLIED
+ >
+
+<!--
+colgroup groups a set of col elements. It allows you to group
+several semantically related columns together.
+-->
+<!ATTLIST colgroup
+ %attrs;
+ span %Number; "1"
+ width %MultiLength; #IMPLIED
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!--
+ col elements define the alignment properties for cells in
+ one or more columns.
+
+ The width attribute specifies the width of the columns, e.g.
+
+ width=64 width in screen pixels
+ width=0.5* relative width of 0.5
+
+ The span attribute causes the attributes of one
+ col element to apply to more than one column.
+-->
+<!ATTLIST col
+ %attrs;
+ span %Number; "1"
+ width %MultiLength; #IMPLIED
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!--
+ Use thead to duplicate headers when breaking table
+ across page boundaries, or for static headers when
+ tbody sections are rendered in scrolling panel.
+
+ Use tfoot to duplicate footers when breaking table
+ across page boundaries, or for static footers when
+ tbody sections are rendered in scrolling panel.
+
+ Use multiple tbody sections when rules are needed
+ between groups of table rows.
+-->
+<!ATTLIST thead
+ %attrs;
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!ATTLIST tfoot
+ %attrs;
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!ATTLIST tbody
+ %attrs;
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!ATTLIST tr
+ %attrs;
+ %cellhalign;
+ %cellvalign;
+ bgcolor %Color; #IMPLIED
+ >
+
+<!-- Scope is simpler than headers attribute for common tables -->
+<!ENTITY % Scope "(row|col|rowgroup|colgroup)">
+
+<!-- th is for headers, td for data and for cells acting as both -->
+
+<!ATTLIST th
+ %attrs;
+ abbr %Text; #IMPLIED
+ axis CDATA #IMPLIED
+ headers IDREFS #IMPLIED
+ scope %Scope; #IMPLIED
+ rowspan %Number; "1"
+ colspan %Number; "1"
+ %cellhalign;
+ %cellvalign;
+ nowrap (nowrap) #IMPLIED
+ bgcolor %Color; #IMPLIED
+ width %Pixels; #IMPLIED
+ height %Pixels; #IMPLIED
+ >
+
+<!ATTLIST td
+ %attrs;
+ abbr %Text; #IMPLIED
+ axis CDATA #IMPLIED
+ headers IDREFS #IMPLIED
+ scope %Scope; #IMPLIED
+ rowspan %Number; "1"
+ colspan %Number; "1"
+ %cellhalign;
+ %cellvalign;
+ nowrap (nowrap) #IMPLIED
+ bgcolor %Color; #IMPLIED
+ width %Pixels; #IMPLIED
+ height %Pixels; #IMPLIED
+ >
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dtd/xhtml1-strict.dtd Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,978 @@
+<!--
+ Extensible HTML version 1.0 Strict DTD
+
+ This is the same as HTML 4 Strict except for
+ changes due to the differences between XML and SGML.
+
+ Namespace = http://www.w3.org/1999/xhtml
+
+ For further information, see: http://www.w3.org/TR/xhtml1
+
+ Copyright (c) 1998-2002 W3C (MIT, INRIA, Keio),
+ All Rights Reserved.
+
+ This DTD module is identified by the PUBLIC and SYSTEM identifiers:
+
+ PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+ SYSTEM "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"
+
+ $Revision$
+ $Date$
+
+-->
+
+<!--================ Character mnemonic entities =========================-->
+
+<!ENTITY % HTMLlat1 PUBLIC
+ "-//W3C//ENTITIES Latin 1 for XHTML//EN"
+ "xhtml-lat1.ent">
+%HTMLlat1;
+
+<!ENTITY % HTMLsymbol PUBLIC
+ "-//W3C//ENTITIES Symbols for XHTML//EN"
+ "xhtml-symbol.ent">
+%HTMLsymbol;
+
+<!ENTITY % HTMLspecial PUBLIC
+ "-//W3C//ENTITIES Special for XHTML//EN"
+ "xhtml-special.ent">
+%HTMLspecial;
+
+<!--================== Imported Names ====================================-->
+
+<!ENTITY % ContentType "CDATA">
+ <!-- media type, as per [RFC2045] -->
+
+<!ENTITY % ContentTypes "CDATA">
+ <!-- comma-separated list of media types, as per [RFC2045] -->
+
+<!ENTITY % Charset "CDATA">
+ <!-- a character encoding, as per [RFC2045] -->
+
+<!ENTITY % Charsets "CDATA">
+ <!-- a space separated list of character encodings, as per [RFC2045] -->
+
+<!ENTITY % LanguageCode "NMTOKEN">
+ <!-- a language code, as per [RFC3066] -->
+
+<!ENTITY % Character "CDATA">
+ <!-- a single character, as per section 2.2 of [XML] -->
+
+<!ENTITY % Number "CDATA">
+ <!-- one or more digits -->
+
+<!ENTITY % LinkTypes "CDATA">
+ <!-- space-separated list of link types -->
+
+<!ENTITY % MediaDesc "CDATA">
+ <!-- single or comma-separated list of media descriptors -->
+
+<!ENTITY % URI "CDATA">
+ <!-- a Uniform Resource Identifier, see [RFC2396] -->
+
+<!ENTITY % UriList "CDATA">
+ <!-- a space separated list of Uniform Resource Identifiers -->
+
+<!ENTITY % Datetime "CDATA">
+ <!-- date and time information. ISO date format -->
+
+<!ENTITY % Script "CDATA">
+ <!-- script expression -->
+
+<!ENTITY % StyleSheet "CDATA">
+ <!-- style sheet data -->
+
+<!ENTITY % Text "CDATA">
+ <!-- used for titles etc. -->
+
+<!ENTITY % Length "CDATA">
+ <!-- nn for pixels or nn% for percentage length -->
+
+<!ENTITY % MultiLength "CDATA">
+ <!-- pixel, percentage, or relative -->
+
+<!ENTITY % Pixels "CDATA">
+ <!-- integer representing length in pixels -->
+
+<!-- these are used for image maps -->
+
+<!ENTITY % Shape "(rect|circle|poly|default)">
+
+<!ENTITY % Coords "CDATA">
+ <!-- comma separated list of lengths -->
+
+<!--=================== Generic Attributes ===============================-->
+
+<!-- core attributes common to most elements
+ id document-wide unique id
+ class space separated list of classes
+ style associated style info
+ title advisory title/amplification
+-->
+<!ENTITY % coreattrs
+ "id ID #IMPLIED
+ class CDATA #IMPLIED
+ style %StyleSheet; #IMPLIED
+ title %Text; #IMPLIED"
+ >
+
+<!-- internationalization attributes
+ lang language code (backwards compatible)
+ xml:lang language code (as per XML 1.0 spec)
+ dir direction for weak/neutral text
+-->
+<!ENTITY % i18n
+ "lang %LanguageCode; #IMPLIED
+ xml:lang %LanguageCode; #IMPLIED
+ dir (ltr|rtl) #IMPLIED"
+ >
+
+<!-- attributes for common UI events
+ onclick a pointer button was clicked
+ ondblclick a pointer button was double clicked
+ onmousedown a pointer button was pressed down
+ onmouseup a pointer button was released
+ onmousemove a pointer was moved onto the element
+ onmouseout a pointer was moved away from the element
+ onkeypress a key was pressed and released
+ onkeydown a key was pressed down
+ onkeyup a key was released
+-->
+<!ENTITY % events
+ "onclick %Script; #IMPLIED
+ ondblclick %Script; #IMPLIED
+ onmousedown %Script; #IMPLIED
+ onmouseup %Script; #IMPLIED
+ onmouseover %Script; #IMPLIED
+ onmousemove %Script; #IMPLIED
+ onmouseout %Script; #IMPLIED
+ onkeypress %Script; #IMPLIED
+ onkeydown %Script; #IMPLIED
+ onkeyup %Script; #IMPLIED"
+ >
+
+<!-- attributes for elements that can get the focus
+ accesskey accessibility key character
+ tabindex position in tabbing order
+ onfocus the element got the focus
+ onblur the element lost the focus
+-->
+<!ENTITY % focus
+ "accesskey %Character; #IMPLIED
+ tabindex %Number; #IMPLIED
+ onfocus %Script; #IMPLIED
+ onblur %Script; #IMPLIED"
+ >
+
+<!ENTITY % attrs "%coreattrs; %i18n; %events;">
+
+<!--=================== Text Elements ====================================-->
+
+<!ENTITY % special.pre
+ "br | span | bdo | map">
+
+
+<!ENTITY % special
+ "%special.pre; | object | img ">
+
+<!ENTITY % fontstyle "tt | i | b | big | small ">
+
+<!ENTITY % phrase "em | strong | dfn | code | q |
+ samp | kbd | var | cite | abbr | acronym | sub | sup ">
+
+<!ENTITY % inline.forms "input | select | textarea | label | button">
+
+<!-- these can occur at block or inline level -->
+<!ENTITY % misc.inline "ins | del | script">
+
+<!-- these can only occur at block level -->
+<!ENTITY % misc "noscript | %misc.inline;">
+
+<!ENTITY % inline "a | %special; | %fontstyle; | %phrase; | %inline.forms;">
+
+<!-- %Inline; covers inline or "text-level" elements -->
+<!ENTITY % Inline "(#PCDATA | %inline; | %misc.inline;)*">
+
+<!--================== Block level elements ==============================-->
+
+<!ENTITY % heading "h1|h2|h3|h4|h5|h6">
+<!ENTITY % lists "ul | ol | dl">
+<!ENTITY % blocktext "pre | hr | blockquote | address">
+
+<!ENTITY % block
+ "p | %heading; | div | %lists; | %blocktext; | fieldset | table">
+
+<!ENTITY % Block "(%block; | form | %misc;)*">
+
+<!-- %Flow; mixes block and inline and is used for list items etc. -->
+<!ENTITY % Flow "(#PCDATA | %block; | form | %inline; | %misc;)*">
+
+<!--================== Content models for exclusions =====================-->
+
+<!-- a elements use %Inline; excluding a -->
+
+<!ENTITY % a.content
+ "(#PCDATA | %special; | %fontstyle; | %phrase; | %inline.forms; | %misc.inline;)*">
+
+<!-- pre uses %Inline excluding big, small, sup or sup -->
+
+<!ENTITY % pre.content
+ "(#PCDATA | a | %fontstyle; | %phrase; | %special.pre; | %misc.inline;
+ | %inline.forms;)*">
+
+<!-- form uses %Block; excluding form -->
+
+<!ENTITY % form.content "(%block; | %misc;)*">
+
+<!-- button uses %Flow; but excludes a, form and form controls -->
+
+<!ENTITY % button.content
+ "(#PCDATA | p | %heading; | div | %lists; | %blocktext; |
+ table | %special; | %fontstyle; | %phrase; | %misc;)*">
+
+<!--================ Document Structure ==================================-->
+
+<!-- the namespace URI designates the document profile -->
+
+<!ELEMENT html (head, body)>
+<!ATTLIST html
+ %i18n;
+ id ID #IMPLIED
+ xmlns %URI; #FIXED 'http://www.w3.org/1999/xhtml'
+ >
+
+<!--================ Document Head =======================================-->
+
+<!ENTITY % head.misc "(script|style|meta|link|object)*">
+
+<!-- content model is %head.misc; combined with a single
+ title and an optional base element in any order -->
+
+<!ELEMENT head (%head.misc;,
+ ((title, %head.misc;, (base, %head.misc;)?) |
+ (base, %head.misc;, (title, %head.misc;))))>
+
+<!ATTLIST head
+ %i18n;
+ id ID #IMPLIED
+ profile %URI; #IMPLIED
+ >
+
+<!-- The title element is not considered part of the flow of text.
+ It should be displayed, for example as the page header or
+ window title. Exactly one title is required per document.
+ -->
+<!ELEMENT title (#PCDATA)>
+<!ATTLIST title
+ %i18n;
+ id ID #IMPLIED
+ >
+
+<!-- document base URI -->
+
+<!ELEMENT base EMPTY>
+<!ATTLIST base
+ href %URI; #REQUIRED
+ id ID #IMPLIED
+ >
+
+<!-- generic metainformation -->
+<!ELEMENT meta EMPTY>
+<!ATTLIST meta
+ %i18n;
+ id ID #IMPLIED
+ http-equiv CDATA #IMPLIED
+ name CDATA #IMPLIED
+ content CDATA #REQUIRED
+ scheme CDATA #IMPLIED
+ >
+
+<!--
+ Relationship values can be used in principle:
+
+ a) for document specific toolbars/menus when used
+ with the link element in document head e.g.
+ start, contents, previous, next, index, end, help
+ b) to link to a separate style sheet (rel="stylesheet")
+ c) to make a link to a script (rel="script")
+ d) by stylesheets to control how collections of
+ html nodes are rendered into printed documents
+ e) to make a link to a printable version of this document
+ e.g. a PostScript or PDF version (rel="alternate" media="print")
+-->
+
+<!ELEMENT link EMPTY>
+<!ATTLIST link
+ %attrs;
+ charset %Charset; #IMPLIED
+ href %URI; #IMPLIED
+ hreflang %LanguageCode; #IMPLIED
+ type %ContentType; #IMPLIED
+ rel %LinkTypes; #IMPLIED
+ rev %LinkTypes; #IMPLIED
+ media %MediaDesc; #IMPLIED
+ >
+
+<!-- style info, which may include CDATA sections -->
+<!ELEMENT style (#PCDATA)>
+<!ATTLIST style
+ %i18n;
+ id ID #IMPLIED
+ type %ContentType; #REQUIRED
+ media %MediaDesc; #IMPLIED
+ title %Text; #IMPLIED
+ xml:space (preserve) #FIXED 'preserve'
+ >
+
+<!-- script statements, which may include CDATA sections -->
+<!ELEMENT script (#PCDATA)>
+<!ATTLIST script
+ id ID #IMPLIED
+ charset %Charset; #IMPLIED
+ type %ContentType; #REQUIRED
+ src %URI; #IMPLIED
+ defer (defer) #IMPLIED
+ xml:space (preserve) #FIXED 'preserve'
+ >
+
+<!-- alternate content container for non script-based rendering -->
+
+<!ELEMENT noscript %Block;>
+<!ATTLIST noscript
+ %attrs;
+ >
+
+<!--=================== Document Body ====================================-->
+
+<!ELEMENT body %Block;>
+<!ATTLIST body
+ %attrs;
+ onload %Script; #IMPLIED
+ onunload %Script; #IMPLIED
+ >
+
+<!ELEMENT div %Flow;> <!-- generic language/style container -->
+<!ATTLIST div
+ %attrs;
+ >
+
+<!--=================== Paragraphs =======================================-->
+
+<!ELEMENT p %Inline;>
+<!ATTLIST p
+ %attrs;
+ >
+
+<!--=================== Headings =========================================-->
+
+<!--
+ There are six levels of headings from h1 (the most important)
+ to h6 (the least important).
+-->
+
+<!ELEMENT h1 %Inline;>
+<!ATTLIST h1
+ %attrs;
+ >
+
+<!ELEMENT h2 %Inline;>
+<!ATTLIST h2
+ %attrs;
+ >
+
+<!ELEMENT h3 %Inline;>
+<!ATTLIST h3
+ %attrs;
+ >
+
+<!ELEMENT h4 %Inline;>
+<!ATTLIST h4
+ %attrs;
+ >
+
+<!ELEMENT h5 %Inline;>
+<!ATTLIST h5
+ %attrs;
+ >
+
+<!ELEMENT h6 %Inline;>
+<!ATTLIST h6
+ %attrs;
+ >
+
+<!--=================== Lists ============================================-->
+
+<!-- Unordered list -->
+
+<!ELEMENT ul (li)+>
+<!ATTLIST ul
+ %attrs;
+ >
+
+<!-- Ordered (numbered) list -->
+
+<!ELEMENT ol (li)+>
+<!ATTLIST ol
+ %attrs;
+ >
+
+<!-- list item -->
+
+<!ELEMENT li %Flow;>
+<!ATTLIST li
+ %attrs;
+ >
+
+<!-- definition lists - dt for term, dd for its definition -->
+
+<!ELEMENT dl (dt|dd)+>
+<!ATTLIST dl
+ %attrs;
+ >
+
+<!ELEMENT dt %Inline;>
+<!ATTLIST dt
+ %attrs;
+ >
+
+<!ELEMENT dd %Flow;>
+<!ATTLIST dd
+ %attrs;
+ >
+
+<!--=================== Address ==========================================-->
+
+<!-- information on author -->
+
+<!ELEMENT address %Inline;>
+<!ATTLIST address
+ %attrs;
+ >
+
+<!--=================== Horizontal Rule ==================================-->
+
+<!ELEMENT hr EMPTY>
+<!ATTLIST hr
+ %attrs;
+ >
+
+<!--=================== Preformatted Text ================================-->
+
+<!-- content is %Inline; excluding "img|object|big|small|sub|sup" -->
+
+<!ELEMENT pre %pre.content;>
+<!ATTLIST pre
+ %attrs;
+ xml:space (preserve) #FIXED 'preserve'
+ >
+
+<!--=================== Block-like Quotes ================================-->
+
+<!ELEMENT blockquote %Block;>
+<!ATTLIST blockquote
+ %attrs;
+ cite %URI; #IMPLIED
+ >
+
+<!--=================== Inserted/Deleted Text ============================-->
+
+<!--
+ ins/del are allowed in block and inline content, but its
+ inappropriate to include block content within an ins element
+ occurring in inline content.
+-->
+<!ELEMENT ins %Flow;>
+<!ATTLIST ins
+ %attrs;
+ cite %URI; #IMPLIED
+ datetime %Datetime; #IMPLIED
+ >
+
+<!ELEMENT del %Flow;>
+<!ATTLIST del
+ %attrs;
+ cite %URI; #IMPLIED
+ datetime %Datetime; #IMPLIED
+ >
+
+<!--================== The Anchor Element ================================-->
+
+<!-- content is %Inline; except that anchors shouldn't be nested -->
+
+<!ELEMENT a %a.content;>
+<!ATTLIST a
+ %attrs;
+ %focus;
+ charset %Charset; #IMPLIED
+ type %ContentType; #IMPLIED
+ name NMTOKEN #IMPLIED
+ href %URI; #IMPLIED
+ hreflang %LanguageCode; #IMPLIED
+ rel %LinkTypes; #IMPLIED
+ rev %LinkTypes; #IMPLIED
+ shape %Shape; "rect"
+ coords %Coords; #IMPLIED
+ >
+
+<!--===================== Inline Elements ================================-->
+
+<!ELEMENT span %Inline;> <!-- generic language/style container -->
+<!ATTLIST span
+ %attrs;
+ >
+
+<!ELEMENT bdo %Inline;> <!-- I18N BiDi over-ride -->
+<!ATTLIST bdo
+ %coreattrs;
+ %events;
+ lang %LanguageCode; #IMPLIED
+ xml:lang %LanguageCode; #IMPLIED
+ dir (ltr|rtl) #REQUIRED
+ >
+
+<!ELEMENT br EMPTY> <!-- forced line break -->
+<!ATTLIST br
+ %coreattrs;
+ >
+
+<!ELEMENT em %Inline;> <!-- emphasis -->
+<!ATTLIST em %attrs;>
+
+<!ELEMENT strong %Inline;> <!-- strong emphasis -->
+<!ATTLIST strong %attrs;>
+
+<!ELEMENT dfn %Inline;> <!-- definitional -->
+<!ATTLIST dfn %attrs;>
+
+<!ELEMENT code %Inline;> <!-- program code -->
+<!ATTLIST code %attrs;>
+
+<!ELEMENT samp %Inline;> <!-- sample -->
+<!ATTLIST samp %attrs;>
+
+<!ELEMENT kbd %Inline;> <!-- something user would type -->
+<!ATTLIST kbd %attrs;>
+
+<!ELEMENT var %Inline;> <!-- variable -->
+<!ATTLIST var %attrs;>
+
+<!ELEMENT cite %Inline;> <!-- citation -->
+<!ATTLIST cite %attrs;>
+
+<!ELEMENT abbr %Inline;> <!-- abbreviation -->
+<!ATTLIST abbr %attrs;>
+
+<!ELEMENT acronym %Inline;> <!-- acronym -->
+<!ATTLIST acronym %attrs;>
+
+<!ELEMENT q %Inline;> <!-- inlined quote -->
+<!ATTLIST q
+ %attrs;
+ cite %URI; #IMPLIED
+ >
+
+<!ELEMENT sub %Inline;> <!-- subscript -->
+<!ATTLIST sub %attrs;>
+
+<!ELEMENT sup %Inline;> <!-- superscript -->
+<!ATTLIST sup %attrs;>
+
+<!ELEMENT tt %Inline;> <!-- fixed pitch font -->
+<!ATTLIST tt %attrs;>
+
+<!ELEMENT i %Inline;> <!-- italic font -->
+<!ATTLIST i %attrs;>
+
+<!ELEMENT b %Inline;> <!-- bold font -->
+<!ATTLIST b %attrs;>
+
+<!ELEMENT big %Inline;> <!-- bigger font -->
+<!ATTLIST big %attrs;>
+
+<!ELEMENT small %Inline;> <!-- smaller font -->
+<!ATTLIST small %attrs;>
+
+<!--==================== Object ======================================-->
+<!--
+ object is used to embed objects as part of HTML pages.
+ param elements should precede other content. Parameters
+ can also be expressed as attribute/value pairs on the
+ object element itself when brevity is desired.
+-->
+
+<!ELEMENT object (#PCDATA | param | %block; | form | %inline; | %misc;)*>
+<!ATTLIST object
+ %attrs;
+ declare (declare) #IMPLIED
+ classid %URI; #IMPLIED
+ codebase %URI; #IMPLIED
+ data %URI; #IMPLIED
+ type %ContentType; #IMPLIED
+ codetype %ContentType; #IMPLIED
+ archive %UriList; #IMPLIED
+ standby %Text; #IMPLIED
+ height %Length; #IMPLIED
+ width %Length; #IMPLIED
+ usemap %URI; #IMPLIED
+ name NMTOKEN #IMPLIED
+ tabindex %Number; #IMPLIED
+ >
+
+<!--
+ param is used to supply a named property value.
+ In XML it would seem natural to follow RDF and support an
+ abbreviated syntax where the param elements are replaced
+ by attribute value pairs on the object start tag.
+-->
+<!ELEMENT param EMPTY>
+<!ATTLIST param
+ id ID #IMPLIED
+ name CDATA #IMPLIED
+ value CDATA #IMPLIED
+ valuetype (data|ref|object) "data"
+ type %ContentType; #IMPLIED
+ >
+
+<!--=================== Images ===========================================-->
+
+<!--
+ To avoid accessibility problems for people who aren't
+ able to see the image, you should provide a text
+ description using the alt and longdesc attributes.
+ In addition, avoid the use of server-side image maps.
+ Note that in this DTD there is no name attribute. That
+ is only available in the transitional and frameset DTD.
+-->
+
+<!ELEMENT img EMPTY>
+<!ATTLIST img
+ %attrs;
+ src %URI; #REQUIRED
+ alt %Text; #REQUIRED
+ longdesc %URI; #IMPLIED
+ height %Length; #IMPLIED
+ width %Length; #IMPLIED
+ usemap %URI; #IMPLIED
+ ismap (ismap) #IMPLIED
+ >
+
+<!-- usemap points to a map element which may be in this document
+ or an external document, although the latter is not widely supported -->
+
+<!--================== Client-side image maps ============================-->
+
+<!-- These can be placed in the same document or grouped in a
+ separate document although this isn't yet widely supported -->
+
+<!ELEMENT map ((%block; | form | %misc;)+ | area+)>
+<!ATTLIST map
+ %i18n;
+ %events;
+ id ID #REQUIRED
+ class CDATA #IMPLIED
+ style %StyleSheet; #IMPLIED
+ title %Text; #IMPLIED
+ name NMTOKEN #IMPLIED
+ >
+
+<!ELEMENT area EMPTY>
+<!ATTLIST area
+ %attrs;
+ %focus;
+ shape %Shape; "rect"
+ coords %Coords; #IMPLIED
+ href %URI; #IMPLIED
+ nohref (nohref) #IMPLIED
+ alt %Text; #REQUIRED
+ >
+
+<!--================ Forms ===============================================-->
+<!ELEMENT form %form.content;> <!-- forms shouldn't be nested -->
+
+<!ATTLIST form
+ %attrs;
+ action %URI; #REQUIRED
+ method (get|post) "get"
+ enctype %ContentType; "application/x-www-form-urlencoded"
+ onsubmit %Script; #IMPLIED
+ onreset %Script; #IMPLIED
+ accept %ContentTypes; #IMPLIED
+ accept-charset %Charsets; #IMPLIED
+ >
+
+<!--
+ Each label must not contain more than ONE field
+ Label elements shouldn't be nested.
+-->
+<!ELEMENT label %Inline;>
+<!ATTLIST label
+ %attrs;
+ for IDREF #IMPLIED
+ accesskey %Character; #IMPLIED
+ onfocus %Script; #IMPLIED
+ onblur %Script; #IMPLIED
+ >
+
+<!ENTITY % InputType
+ "(text | password | checkbox |
+ radio | submit | reset |
+ file | hidden | image | button)"
+ >
+
+<!-- the name attribute is required for all but submit & reset -->
+
+<!ELEMENT input EMPTY> <!-- form control -->
+<!ATTLIST input
+ %attrs;
+ %focus;
+ type %InputType; "text"
+ name CDATA #IMPLIED
+ value CDATA #IMPLIED
+ checked (checked) #IMPLIED
+ disabled (disabled) #IMPLIED
+ readonly (readonly) #IMPLIED
+ size CDATA #IMPLIED
+ maxlength %Number; #IMPLIED
+ src %URI; #IMPLIED
+ alt CDATA #IMPLIED
+ usemap %URI; #IMPLIED
+ onselect %Script; #IMPLIED
+ onchange %Script; #IMPLIED
+ accept %ContentTypes; #IMPLIED
+ >
+
+<!ELEMENT select (optgroup|option)+> <!-- option selector -->
+<!ATTLIST select
+ %attrs;
+ name CDATA #IMPLIED
+ size %Number; #IMPLIED
+ multiple (multiple) #IMPLIED
+ disabled (disabled) #IMPLIED
+ tabindex %Number; #IMPLIED
+ onfocus %Script; #IMPLIED
+ onblur %Script; #IMPLIED
+ onchange %Script; #IMPLIED
+ >
+
+<!ELEMENT optgroup (option)+> <!-- option group -->
+<!ATTLIST optgroup
+ %attrs;
+ disabled (disabled) #IMPLIED
+ label %Text; #REQUIRED
+ >
+
+<!ELEMENT option (#PCDATA)> <!-- selectable choice -->
+<!ATTLIST option
+ %attrs;
+ selected (selected) #IMPLIED
+ disabled (disabled) #IMPLIED
+ label %Text; #IMPLIED
+ value CDATA #IMPLIED
+ >
+
+<!ELEMENT textarea (#PCDATA)> <!-- multi-line text field -->
+<!ATTLIST textarea
+ %attrs;
+ %focus;
+ name CDATA #IMPLIED
+ rows %Number; #REQUIRED
+ cols %Number; #REQUIRED
+ disabled (disabled) #IMPLIED
+ readonly (readonly) #IMPLIED
+ onselect %Script; #IMPLIED
+ onchange %Script; #IMPLIED
+ >
+
+<!--
+ The fieldset element is used to group form fields.
+ Only one legend element should occur in the content
+ and if present should only be preceded by whitespace.
+-->
+<!ELEMENT fieldset (#PCDATA | legend | %block; | form | %inline; | %misc;)*>
+<!ATTLIST fieldset
+ %attrs;
+ >
+
+<!ELEMENT legend %Inline;> <!-- fieldset label -->
+<!ATTLIST legend
+ %attrs;
+ accesskey %Character; #IMPLIED
+ >
+
+<!--
+ Content is %Flow; excluding a, form and form controls
+-->
+<!ELEMENT button %button.content;> <!-- push button -->
+<!ATTLIST button
+ %attrs;
+ %focus;
+ name CDATA #IMPLIED
+ value CDATA #IMPLIED
+ type (button|submit|reset) "submit"
+ disabled (disabled) #IMPLIED
+ >
+
+<!--======================= Tables =======================================-->
+
+<!-- Derived from IETF HTML table standard, see [RFC1942] -->
+
+<!--
+ The border attribute sets the thickness of the frame around the
+ table. The default units are screen pixels.
+
+ The frame attribute specifies which parts of the frame around
+ the table should be rendered. The values are not the same as
+ CALS to avoid a name clash with the valign attribute.
+-->
+<!ENTITY % TFrame "(void|above|below|hsides|lhs|rhs|vsides|box|border)">
+
+<!--
+ The rules attribute defines which rules to draw between cells:
+
+ If rules is absent then assume:
+ "none" if border is absent or border="0" otherwise "all"
+-->
+
+<!ENTITY % TRules "(none | groups | rows | cols | all)">
+
+<!-- horizontal alignment attributes for cell contents
+
+ char alignment char, e.g. char=':'
+ charoff offset for alignment char
+-->
+<!ENTITY % cellhalign
+ "align (left|center|right|justify|char) #IMPLIED
+ char %Character; #IMPLIED
+ charoff %Length; #IMPLIED"
+ >
+
+<!-- vertical alignment attributes for cell contents -->
+<!ENTITY % cellvalign
+ "valign (top|middle|bottom|baseline) #IMPLIED"
+ >
+
+<!ELEMENT table
+ (caption?, (col*|colgroup*), thead?, tfoot?, (tbody+|tr+))>
+<!ELEMENT caption %Inline;>
+<!ELEMENT thead (tr)+>
+<!ELEMENT tfoot (tr)+>
+<!ELEMENT tbody (tr)+>
+<!ELEMENT colgroup (col)*>
+<!ELEMENT col EMPTY>
+<!ELEMENT tr (th|td)+>
+<!ELEMENT th %Flow;>
+<!ELEMENT td %Flow;>
+
+<!ATTLIST table
+ %attrs;
+ summary %Text; #IMPLIED
+ width %Length; #IMPLIED
+ border %Pixels; #IMPLIED
+ frame %TFrame; #IMPLIED
+ rules %TRules; #IMPLIED
+ cellspacing %Length; #IMPLIED
+ cellpadding %Length; #IMPLIED
+ >
+
+<!ATTLIST caption
+ %attrs;
+ >
+
+<!--
+colgroup groups a set of col elements. It allows you to group
+several semantically related columns together.
+-->
+<!ATTLIST colgroup
+ %attrs;
+ span %Number; "1"
+ width %MultiLength; #IMPLIED
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!--
+ col elements define the alignment properties for cells in
+ one or more columns.
+
+ The width attribute specifies the width of the columns, e.g.
+
+ width=64 width in screen pixels
+ width=0.5* relative width of 0.5
+
+ The span attribute causes the attributes of one
+ col element to apply to more than one column.
+-->
+<!ATTLIST col
+ %attrs;
+ span %Number; "1"
+ width %MultiLength; #IMPLIED
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!--
+ Use thead to duplicate headers when breaking table
+ across page boundaries, or for static headers when
+ tbody sections are rendered in scrolling panel.
+
+ Use tfoot to duplicate footers when breaking table
+ across page boundaries, or for static footers when
+ tbody sections are rendered in scrolling panel.
+
+ Use multiple tbody sections when rules are needed
+ between groups of table rows.
+-->
+<!ATTLIST thead
+ %attrs;
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!ATTLIST tfoot
+ %attrs;
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!ATTLIST tbody
+ %attrs;
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!ATTLIST tr
+ %attrs;
+ %cellhalign;
+ %cellvalign;
+ >
+
+
+<!-- Scope is simpler than headers attribute for common tables -->
+<!ENTITY % Scope "(row|col|rowgroup|colgroup)">
+
+<!-- th is for headers, td for data and for cells acting as both -->
+
+<!ATTLIST th
+ %attrs;
+ abbr %Text; #IMPLIED
+ axis CDATA #IMPLIED
+ headers IDREFS #IMPLIED
+ scope %Scope; #IMPLIED
+ rowspan %Number; "1"
+ colspan %Number; "1"
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!ATTLIST td
+ %attrs;
+ abbr %Text; #IMPLIED
+ axis CDATA #IMPLIED
+ headers IDREFS #IMPLIED
+ scope %Scope; #IMPLIED
+ rowspan %Number; "1"
+ colspan %Number; "1"
+ %cellhalign;
+ %cellvalign;
+ >
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/dtd/xhtml1-transitional.dtd Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,1201 @@
+<!--
+ Extensible HTML version 1.0 Transitional DTD
+
+ This is the same as HTML 4 Transitional except for
+ changes due to the differences between XML and SGML.
+
+ Namespace = http://www.w3.org/1999/xhtml
+
+ For further information, see: http://www.w3.org/TR/xhtml1
+
+ Copyright (c) 1998-2002 W3C (MIT, INRIA, Keio),
+ All Rights Reserved.
+
+ This DTD module is identified by the PUBLIC and SYSTEM identifiers:
+
+ PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+ SYSTEM "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"
+
+ $Revision$
+ $Date$
+
+-->
+
+<!--================ Character mnemonic entities =========================-->
+
+<!ENTITY % HTMLlat1 PUBLIC
+ "-//W3C//ENTITIES Latin 1 for XHTML//EN"
+ "xhtml-lat1.ent">
+%HTMLlat1;
+
+<!ENTITY % HTMLsymbol PUBLIC
+ "-//W3C//ENTITIES Symbols for XHTML//EN"
+ "xhtml-symbol.ent">
+%HTMLsymbol;
+
+<!ENTITY % HTMLspecial PUBLIC
+ "-//W3C//ENTITIES Special for XHTML//EN"
+ "xhtml-special.ent">
+%HTMLspecial;
+
+<!--================== Imported Names ====================================-->
+
+<!ENTITY % ContentType "CDATA">
+ <!-- media type, as per [RFC2045] -->
+
+<!ENTITY % ContentTypes "CDATA">
+ <!-- comma-separated list of media types, as per [RFC2045] -->
+
+<!ENTITY % Charset "CDATA">
+ <!-- a character encoding, as per [RFC2045] -->
+
+<!ENTITY % Charsets "CDATA">
+ <!-- a space separated list of character encodings, as per [RFC2045] -->
+
+<!ENTITY % LanguageCode "NMTOKEN">
+ <!-- a language code, as per [RFC3066] -->
+
+<!ENTITY % Character "CDATA">
+ <!-- a single character, as per section 2.2 of [XML] -->
+
+<!ENTITY % Number "CDATA">
+ <!-- one or more digits -->
+
+<!ENTITY % LinkTypes "CDATA">
+ <!-- space-separated list of link types -->
+
+<!ENTITY % MediaDesc "CDATA">
+ <!-- single or comma-separated list of media descriptors -->
+
+<!ENTITY % URI "CDATA">
+ <!-- a Uniform Resource Identifier, see [RFC2396] -->
+
+<!ENTITY % UriList "CDATA">
+ <!-- a space separated list of Uniform Resource Identifiers -->
+
+<!ENTITY % Datetime "CDATA">
+ <!-- date and time information. ISO date format -->
+
+<!ENTITY % Script "CDATA">
+ <!-- script expression -->
+
+<!ENTITY % StyleSheet "CDATA">
+ <!-- style sheet data -->
+
+<!ENTITY % Text "CDATA">
+ <!-- used for titles etc. -->
+
+<!ENTITY % FrameTarget "NMTOKEN">
+ <!-- render in this frame -->
+
+<!ENTITY % Length "CDATA">
+ <!-- nn for pixels or nn% for percentage length -->
+
+<!ENTITY % MultiLength "CDATA">
+ <!-- pixel, percentage, or relative -->
+
+<!ENTITY % Pixels "CDATA">
+ <!-- integer representing length in pixels -->
+
+<!-- these are used for image maps -->
+
+<!ENTITY % Shape "(rect|circle|poly|default)">
+
+<!ENTITY % Coords "CDATA">
+ <!-- comma separated list of lengths -->
+
+<!-- used for object, applet, img, input and iframe -->
+<!ENTITY % ImgAlign "(top|middle|bottom|left|right)">
+
+<!-- a color using sRGB: #RRGGBB as Hex values -->
+<!ENTITY % Color "CDATA">
+
+<!-- There are also 16 widely known color names with their sRGB values:
+
+ Black = #000000 Green = #008000
+ Silver = #C0C0C0 Lime = #00FF00
+ Gray = #808080 Olive = #808000
+ White = #FFFFFF Yellow = #FFFF00
+ Maroon = #800000 Navy = #000080
+ Red = #FF0000 Blue = #0000FF
+ Purple = #800080 Teal = #008080
+ Fuchsia= #FF00FF Aqua = #00FFFF
+-->
+
+<!--=================== Generic Attributes ===============================-->
+
+<!-- core attributes common to most elements
+ id document-wide unique id
+ class space separated list of classes
+ style associated style info
+ title advisory title/amplification
+-->
+<!ENTITY % coreattrs
+ "id ID #IMPLIED
+ class CDATA #IMPLIED
+ style %StyleSheet; #IMPLIED
+ title %Text; #IMPLIED"
+ >
+
+<!-- internationalization attributes
+ lang language code (backwards compatible)
+ xml:lang language code (as per XML 1.0 spec)
+ dir direction for weak/neutral text
+-->
+<!ENTITY % i18n
+ "lang %LanguageCode; #IMPLIED
+ xml:lang %LanguageCode; #IMPLIED
+ dir (ltr|rtl) #IMPLIED"
+ >
+
+<!-- attributes for common UI events
+ onclick a pointer button was clicked
+ ondblclick a pointer button was double clicked
+ onmousedown a pointer button was pressed down
+ onmouseup a pointer button was released
+ onmousemove a pointer was moved onto the element
+ onmouseout a pointer was moved away from the element
+ onkeypress a key was pressed and released
+ onkeydown a key was pressed down
+ onkeyup a key was released
+-->
+<!ENTITY % events
+ "onclick %Script; #IMPLIED
+ ondblclick %Script; #IMPLIED
+ onmousedown %Script; #IMPLIED
+ onmouseup %Script; #IMPLIED
+ onmouseover %Script; #IMPLIED
+ onmousemove %Script; #IMPLIED
+ onmouseout %Script; #IMPLIED
+ onkeypress %Script; #IMPLIED
+ onkeydown %Script; #IMPLIED
+ onkeyup %Script; #IMPLIED"
+ >
+
+<!-- attributes for elements that can get the focus
+ accesskey accessibility key character
+ tabindex position in tabbing order
+ onfocus the element got the focus
+ onblur the element lost the focus
+-->
+<!ENTITY % focus
+ "accesskey %Character; #IMPLIED
+ tabindex %Number; #IMPLIED
+ onfocus %Script; #IMPLIED
+ onblur %Script; #IMPLIED"
+ >
+
+<!ENTITY % attrs "%coreattrs; %i18n; %events;">
+
+<!-- text alignment for p, div, h1-h6. The default is
+ align="left" for ltr headings, "right" for rtl -->
+
+<!ENTITY % TextAlign "align (left|center|right|justify) #IMPLIED">
+
+<!--=================== Text Elements ====================================-->
+
+<!ENTITY % special.extra
+ "object | applet | img | map | iframe">
+
+<!ENTITY % special.basic
+ "br | span | bdo">
+
+<!ENTITY % special
+ "%special.basic; | %special.extra;">
+
+<!ENTITY % fontstyle.extra "big | small | font | basefont">
+
+<!ENTITY % fontstyle.basic "tt | i | b | u
+ | s | strike ">
+
+<!ENTITY % fontstyle "%fontstyle.basic; | %fontstyle.extra;">
+
+<!ENTITY % phrase.extra "sub | sup">
+<!ENTITY % phrase.basic "em | strong | dfn | code | q |
+ samp | kbd | var | cite | abbr | acronym">
+
+<!ENTITY % phrase "%phrase.basic; | %phrase.extra;">
+
+<!ENTITY % inline.forms "input | select | textarea | label | button">
+
+<!-- these can occur at block or inline level -->
+<!ENTITY % misc.inline "ins | del | script">
+
+<!-- these can only occur at block level -->
+<!ENTITY % misc "noscript | %misc.inline;">
+
+<!ENTITY % inline "a | %special; | %fontstyle; | %phrase; | %inline.forms;">
+
+<!-- %Inline; covers inline or "text-level" elements -->
+<!ENTITY % Inline "(#PCDATA | %inline; | %misc.inline;)*">
+
+<!--================== Block level elements ==============================-->
+
+<!ENTITY % heading "h1|h2|h3|h4|h5|h6">
+<!ENTITY % lists "ul | ol | dl | menu | dir">
+<!ENTITY % blocktext "pre | hr | blockquote | address | center | noframes">
+
+<!ENTITY % block
+ "p | %heading; | div | %lists; | %blocktext; | isindex |fieldset | table">
+
+<!-- %Flow; mixes block and inline and is used for list items etc. -->
+<!ENTITY % Flow "(#PCDATA | %block; | form | %inline; | %misc;)*">
+
+<!--================== Content models for exclusions =====================-->
+
+<!-- a elements use %Inline; excluding a -->
+
+<!ENTITY % a.content
+ "(#PCDATA | %special; | %fontstyle; | %phrase; | %inline.forms; | %misc.inline;)*">
+
+<!-- pre uses %Inline excluding img, object, applet, big, small,
+ font, or basefont -->
+
+<!ENTITY % pre.content
+ "(#PCDATA | a | %special.basic; | %fontstyle.basic; | %phrase.basic; |
+ %inline.forms; | %misc.inline;)*">
+
+<!-- form uses %Flow; excluding form -->
+
+<!ENTITY % form.content "(#PCDATA | %block; | %inline; | %misc;)*">
+
+<!-- button uses %Flow; but excludes a, form, form controls, iframe -->
+
+<!ENTITY % button.content
+ "(#PCDATA | p | %heading; | div | %lists; | %blocktext; |
+ table | br | span | bdo | object | applet | img | map |
+ %fontstyle; | %phrase; | %misc;)*">
+
+<!--================ Document Structure ==================================-->
+
+<!-- the namespace URI designates the document profile -->
+
+<!ELEMENT html (head, body)>
+<!ATTLIST html
+ %i18n;
+ id ID #IMPLIED
+ xmlns %URI; #FIXED 'http://www.w3.org/1999/xhtml'
+ >
+
+<!--================ Document Head =======================================-->
+
+<!ENTITY % head.misc "(script|style|meta|link|object|isindex)*">
+
+<!-- content model is %head.misc; combined with a single
+ title and an optional base element in any order -->
+
+<!ELEMENT head (%head.misc;,
+ ((title, %head.misc;, (base, %head.misc;)?) |
+ (base, %head.misc;, (title, %head.misc;))))>
+
+<!ATTLIST head
+ %i18n;
+ id ID #IMPLIED
+ profile %URI; #IMPLIED
+ >
+
+<!-- The title element is not considered part of the flow of text.
+ It should be displayed, for example as the page header or
+ window title. Exactly one title is required per document.
+ -->
+<!ELEMENT title (#PCDATA)>
+<!ATTLIST title
+ %i18n;
+ id ID #IMPLIED
+ >
+
+<!-- document base URI -->
+
+<!ELEMENT base EMPTY>
+<!ATTLIST base
+ id ID #IMPLIED
+ href %URI; #IMPLIED
+ target %FrameTarget; #IMPLIED
+ >
+
+<!-- generic metainformation -->
+<!ELEMENT meta EMPTY>
+<!ATTLIST meta
+ %i18n;
+ id ID #IMPLIED
+ http-equiv CDATA #IMPLIED
+ name CDATA #IMPLIED
+ content CDATA #REQUIRED
+ scheme CDATA #IMPLIED
+ >
+
+<!--
+ Relationship values can be used in principle:
+
+ a) for document specific toolbars/menus when used
+ with the link element in document head e.g.
+ start, contents, previous, next, index, end, help
+ b) to link to a separate style sheet (rel="stylesheet")
+ c) to make a link to a script (rel="script")
+ d) by stylesheets to control how collections of
+ html nodes are rendered into printed documents
+ e) to make a link to a printable version of this document
+ e.g. a PostScript or PDF version (rel="alternate" media="print")
+-->
+
+<!ELEMENT link EMPTY>
+<!ATTLIST link
+ %attrs;
+ charset %Charset; #IMPLIED
+ href %URI; #IMPLIED
+ hreflang %LanguageCode; #IMPLIED
+ type %ContentType; #IMPLIED
+ rel %LinkTypes; #IMPLIED
+ rev %LinkTypes; #IMPLIED
+ media %MediaDesc; #IMPLIED
+ target %FrameTarget; #IMPLIED
+ >
+
+<!-- style info, which may include CDATA sections -->
+<!ELEMENT style (#PCDATA)>
+<!ATTLIST style
+ %i18n;
+ id ID #IMPLIED
+ type %ContentType; #REQUIRED
+ media %MediaDesc; #IMPLIED
+ title %Text; #IMPLIED
+ xml:space (preserve) #FIXED 'preserve'
+ >
+
+<!-- script statements, which may include CDATA sections -->
+<!ELEMENT script (#PCDATA)>
+<!ATTLIST script
+ id ID #IMPLIED
+ charset %Charset; #IMPLIED
+ type %ContentType; #REQUIRED
+ language CDATA #IMPLIED
+ src %URI; #IMPLIED
+ defer (defer) #IMPLIED
+ xml:space (preserve) #FIXED 'preserve'
+ >
+
+<!-- alternate content container for non script-based rendering -->
+
+<!ELEMENT noscript %Flow;>
+<!ATTLIST noscript
+ %attrs;
+ >
+
+<!--======================= Frames =======================================-->
+
+<!-- inline subwindow -->
+
+<!ELEMENT iframe %Flow;>
+<!ATTLIST iframe
+ %coreattrs;
+ longdesc %URI; #IMPLIED
+ name NMTOKEN #IMPLIED
+ src %URI; #IMPLIED
+ frameborder (1|0) "1"
+ marginwidth %Pixels; #IMPLIED
+ marginheight %Pixels; #IMPLIED
+ scrolling (yes|no|auto) "auto"
+ align %ImgAlign; #IMPLIED
+ height %Length; #IMPLIED
+ width %Length; #IMPLIED
+ >
+
+<!-- alternate content container for non frame-based rendering -->
+
+<!ELEMENT noframes %Flow;>
+<!ATTLIST noframes
+ %attrs;
+ >
+
+<!--=================== Document Body ====================================-->
+
+<!ELEMENT body %Flow;>
+<!ATTLIST body
+ %attrs;
+ onload %Script; #IMPLIED
+ onunload %Script; #IMPLIED
+ background %URI; #IMPLIED
+ bgcolor %Color; #IMPLIED
+ text %Color; #IMPLIED
+ link %Color; #IMPLIED
+ vlink %Color; #IMPLIED
+ alink %Color; #IMPLIED
+ >
+
+<!ELEMENT div %Flow;> <!-- generic language/style container -->
+<!ATTLIST div
+ %attrs;
+ %TextAlign;
+ >
+
+<!--=================== Paragraphs =======================================-->
+
+<!ELEMENT p %Inline;>
+<!ATTLIST p
+ %attrs;
+ %TextAlign;
+ >
+
+<!--=================== Headings =========================================-->
+
+<!--
+ There are six levels of headings from h1 (the most important)
+ to h6 (the least important).
+-->
+
+<!ELEMENT h1 %Inline;>
+<!ATTLIST h1
+ %attrs;
+ %TextAlign;
+ >
+
+<!ELEMENT h2 %Inline;>
+<!ATTLIST h2
+ %attrs;
+ %TextAlign;
+ >
+
+<!ELEMENT h3 %Inline;>
+<!ATTLIST h3
+ %attrs;
+ %TextAlign;
+ >
+
+<!ELEMENT h4 %Inline;>
+<!ATTLIST h4
+ %attrs;
+ %TextAlign;
+ >
+
+<!ELEMENT h5 %Inline;>
+<!ATTLIST h5
+ %attrs;
+ %TextAlign;
+ >
+
+<!ELEMENT h6 %Inline;>
+<!ATTLIST h6
+ %attrs;
+ %TextAlign;
+ >
+
+<!--=================== Lists ============================================-->
+
+<!-- Unordered list bullet styles -->
+
+<!ENTITY % ULStyle "(disc|square|circle)">
+
+<!-- Unordered list -->
+
+<!ELEMENT ul (li)+>
+<!ATTLIST ul
+ %attrs;
+ type %ULStyle; #IMPLIED
+ compact (compact) #IMPLIED
+ >
+
+<!-- Ordered list numbering style
+
+ 1 arabic numbers 1, 2, 3, ...
+ a lower alpha a, b, c, ...
+ A upper alpha A, B, C, ...
+ i lower roman i, ii, iii, ...
+ I upper roman I, II, III, ...
+
+ The style is applied to the sequence number which by default
+ is reset to 1 for the first list item in an ordered list.
+-->
+<!ENTITY % OLStyle "CDATA">
+
+<!-- Ordered (numbered) list -->
+
+<!ELEMENT ol (li)+>
+<!ATTLIST ol
+ %attrs;
+ type %OLStyle; #IMPLIED
+ compact (compact) #IMPLIED
+ start %Number; #IMPLIED
+ >
+
+<!-- single column list (DEPRECATED) -->
+<!ELEMENT menu (li)+>
+<!ATTLIST menu
+ %attrs;
+ compact (compact) #IMPLIED
+ >
+
+<!-- multiple column list (DEPRECATED) -->
+<!ELEMENT dir (li)+>
+<!ATTLIST dir
+ %attrs;
+ compact (compact) #IMPLIED
+ >
+
+<!-- LIStyle is constrained to: "(%ULStyle;|%OLStyle;)" -->
+<!ENTITY % LIStyle "CDATA">
+
+<!-- list item -->
+
+<!ELEMENT li %Flow;>
+<!ATTLIST li
+ %attrs;
+ type %LIStyle; #IMPLIED
+ value %Number; #IMPLIED
+ >
+
+<!-- definition lists - dt for term, dd for its definition -->
+
+<!ELEMENT dl (dt|dd)+>
+<!ATTLIST dl
+ %attrs;
+ compact (compact) #IMPLIED
+ >
+
+<!ELEMENT dt %Inline;>
+<!ATTLIST dt
+ %attrs;
+ >
+
+<!ELEMENT dd %Flow;>
+<!ATTLIST dd
+ %attrs;
+ >
+
+<!--=================== Address ==========================================-->
+
+<!-- information on author -->
+
+<!ELEMENT address (#PCDATA | %inline; | %misc.inline; | p)*>
+<!ATTLIST address
+ %attrs;
+ >
+
+<!--=================== Horizontal Rule ==================================-->
+
+<!ELEMENT hr EMPTY>
+<!ATTLIST hr
+ %attrs;
+ align (left|center|right) #IMPLIED
+ noshade (noshade) #IMPLIED
+ size %Pixels; #IMPLIED
+ width %Length; #IMPLIED
+ >
+
+<!--=================== Preformatted Text ================================-->
+
+<!-- content is %Inline; excluding
+ "img|object|applet|big|small|sub|sup|font|basefont" -->
+
+<!ELEMENT pre %pre.content;>
+<!ATTLIST pre
+ %attrs;
+ width %Number; #IMPLIED
+ xml:space (preserve) #FIXED 'preserve'
+ >
+
+<!--=================== Block-like Quotes ================================-->
+
+<!ELEMENT blockquote %Flow;>
+<!ATTLIST blockquote
+ %attrs;
+ cite %URI; #IMPLIED
+ >
+
+<!--=================== Text alignment ===================================-->
+
+<!-- center content -->
+<!ELEMENT center %Flow;>
+<!ATTLIST center
+ %attrs;
+ >
+
+<!--=================== Inserted/Deleted Text ============================-->
+
+<!--
+ ins/del are allowed in block and inline content, but its
+ inappropriate to include block content within an ins element
+ occurring in inline content.
+-->
+<!ELEMENT ins %Flow;>
+<!ATTLIST ins
+ %attrs;
+ cite %URI; #IMPLIED
+ datetime %Datetime; #IMPLIED
+ >
+
+<!ELEMENT del %Flow;>
+<!ATTLIST del
+ %attrs;
+ cite %URI; #IMPLIED
+ datetime %Datetime; #IMPLIED
+ >
+
+<!--================== The Anchor Element ================================-->
+
+<!-- content is %Inline; except that anchors shouldn't be nested -->
+
+<!ELEMENT a %a.content;>
+<!ATTLIST a
+ %attrs;
+ %focus;
+ charset %Charset; #IMPLIED
+ type %ContentType; #IMPLIED
+ name NMTOKEN #IMPLIED
+ href %URI; #IMPLIED
+ hreflang %LanguageCode; #IMPLIED
+ rel %LinkTypes; #IMPLIED
+ rev %LinkTypes; #IMPLIED
+ shape %Shape; "rect"
+ coords %Coords; #IMPLIED
+ target %FrameTarget; #IMPLIED
+ >
+
+<!--===================== Inline Elements ================================-->
+
+<!ELEMENT span %Inline;> <!-- generic language/style container -->
+<!ATTLIST span
+ %attrs;
+ >
+
+<!ELEMENT bdo %Inline;> <!-- I18N BiDi over-ride -->
+<!ATTLIST bdo
+ %coreattrs;
+ %events;
+ lang %LanguageCode; #IMPLIED
+ xml:lang %LanguageCode; #IMPLIED
+ dir (ltr|rtl) #REQUIRED
+ >
+
+<!ELEMENT br EMPTY> <!-- forced line break -->
+<!ATTLIST br
+ %coreattrs;
+ clear (left|all|right|none) "none"
+ >
+
+<!ELEMENT em %Inline;> <!-- emphasis -->
+<!ATTLIST em %attrs;>
+
+<!ELEMENT strong %Inline;> <!-- strong emphasis -->
+<!ATTLIST strong %attrs;>
+
+<!ELEMENT dfn %Inline;> <!-- definitional -->
+<!ATTLIST dfn %attrs;>
+
+<!ELEMENT code %Inline;> <!-- program code -->
+<!ATTLIST code %attrs;>
+
+<!ELEMENT samp %Inline;> <!-- sample -->
+<!ATTLIST samp %attrs;>
+
+<!ELEMENT kbd %Inline;> <!-- something user would type -->
+<!ATTLIST kbd %attrs;>
+
+<!ELEMENT var %Inline;> <!-- variable -->
+<!ATTLIST var %attrs;>
+
+<!ELEMENT cite %Inline;> <!-- citation -->
+<!ATTLIST cite %attrs;>
+
+<!ELEMENT abbr %Inline;> <!-- abbreviation -->
+<!ATTLIST abbr %attrs;>
+
+<!ELEMENT acronym %Inline;> <!-- acronym -->
+<!ATTLIST acronym %attrs;>
+
+<!ELEMENT q %Inline;> <!-- inlined quote -->
+<!ATTLIST q
+ %attrs;
+ cite %URI; #IMPLIED
+ >
+
+<!ELEMENT sub %Inline;> <!-- subscript -->
+<!ATTLIST sub %attrs;>
+
+<!ELEMENT sup %Inline;> <!-- superscript -->
+<!ATTLIST sup %attrs;>
+
+<!ELEMENT tt %Inline;> <!-- fixed pitch font -->
+<!ATTLIST tt %attrs;>
+
+<!ELEMENT i %Inline;> <!-- italic font -->
+<!ATTLIST i %attrs;>
+
+<!ELEMENT b %Inline;> <!-- bold font -->
+<!ATTLIST b %attrs;>
+
+<!ELEMENT big %Inline;> <!-- bigger font -->
+<!ATTLIST big %attrs;>
+
+<!ELEMENT small %Inline;> <!-- smaller font -->
+<!ATTLIST small %attrs;>
+
+<!ELEMENT u %Inline;> <!-- underline -->
+<!ATTLIST u %attrs;>
+
+<!ELEMENT s %Inline;> <!-- strike-through -->
+<!ATTLIST s %attrs;>
+
+<!ELEMENT strike %Inline;> <!-- strike-through -->
+<!ATTLIST strike %attrs;>
+
+<!ELEMENT basefont EMPTY> <!-- base font size -->
+<!ATTLIST basefont
+ id ID #IMPLIED
+ size CDATA #REQUIRED
+ color %Color; #IMPLIED
+ face CDATA #IMPLIED
+ >
+
+<!ELEMENT font %Inline;> <!-- local change to font -->
+<!ATTLIST font
+ %coreattrs;
+ %i18n;
+ size CDATA #IMPLIED
+ color %Color; #IMPLIED
+ face CDATA #IMPLIED
+ >
+
+<!--==================== Object ======================================-->
+<!--
+ object is used to embed objects as part of HTML pages.
+ param elements should precede other content. Parameters
+ can also be expressed as attribute/value pairs on the
+ object element itself when brevity is desired.
+-->
+
+<!ELEMENT object (#PCDATA | param | %block; | form | %inline; | %misc;)*>
+<!ATTLIST object
+ %attrs;
+ declare (declare) #IMPLIED
+ classid %URI; #IMPLIED
+ codebase %URI; #IMPLIED
+ data %URI; #IMPLIED
+ type %ContentType; #IMPLIED
+ codetype %ContentType; #IMPLIED
+ archive %UriList; #IMPLIED
+ standby %Text; #IMPLIED
+ height %Length; #IMPLIED
+ width %Length; #IMPLIED
+ usemap %URI; #IMPLIED
+ name NMTOKEN #IMPLIED
+ tabindex %Number; #IMPLIED
+ align %ImgAlign; #IMPLIED
+ border %Pixels; #IMPLIED
+ hspace %Pixels; #IMPLIED
+ vspace %Pixels; #IMPLIED
+ >
+
+<!--
+ param is used to supply a named property value.
+ In XML it would seem natural to follow RDF and support an
+ abbreviated syntax where the param elements are replaced
+ by attribute value pairs on the object start tag.
+-->
+<!ELEMENT param EMPTY>
+<!ATTLIST param
+ id ID #IMPLIED
+ name CDATA #REQUIRED
+ value CDATA #IMPLIED
+ valuetype (data|ref|object) "data"
+ type %ContentType; #IMPLIED
+ >
+
+<!--=================== Java applet ==================================-->
+<!--
+ One of code or object attributes must be present.
+ Place param elements before other content.
+-->
+<!ELEMENT applet (#PCDATA | param | %block; | form | %inline; | %misc;)*>
+<!ATTLIST applet
+ %coreattrs;
+ codebase %URI; #IMPLIED
+ archive CDATA #IMPLIED
+ code CDATA #IMPLIED
+ object CDATA #IMPLIED
+ alt %Text; #IMPLIED
+ name NMTOKEN #IMPLIED
+ width %Length; #REQUIRED
+ height %Length; #REQUIRED
+ align %ImgAlign; #IMPLIED
+ hspace %Pixels; #IMPLIED
+ vspace %Pixels; #IMPLIED
+ >
+
+<!--=================== Images ===========================================-->
+
+<!--
+ To avoid accessibility problems for people who aren't
+ able to see the image, you should provide a text
+ description using the alt and longdesc attributes.
+ In addition, avoid the use of server-side image maps.
+-->
+
+<!ELEMENT img EMPTY>
+<!ATTLIST img
+ %attrs;
+ src %URI; #REQUIRED
+ alt %Text; #REQUIRED
+ name NMTOKEN #IMPLIED
+ longdesc %URI; #IMPLIED
+ height %Length; #IMPLIED
+ width %Length; #IMPLIED
+ usemap %URI; #IMPLIED
+ ismap (ismap) #IMPLIED
+ align %ImgAlign; #IMPLIED
+ border %Length; #IMPLIED
+ hspace %Pixels; #IMPLIED
+ vspace %Pixels; #IMPLIED
+ >
+
+<!-- usemap points to a map element which may be in this document
+ or an external document, although the latter is not widely supported -->
+
+<!--================== Client-side image maps ============================-->
+
+<!-- These can be placed in the same document or grouped in a
+ separate document although this isn't yet widely supported -->
+
+<!ELEMENT map ((%block; | form | %misc;)+ | area+)>
+<!ATTLIST map
+ %i18n;
+ %events;
+ id ID #REQUIRED
+ class CDATA #IMPLIED
+ style %StyleSheet; #IMPLIED
+ title %Text; #IMPLIED
+ name CDATA #IMPLIED
+ >
+
+<!ELEMENT area EMPTY>
+<!ATTLIST area
+ %attrs;
+ %focus;
+ shape %Shape; "rect"
+ coords %Coords; #IMPLIED
+ href %URI; #IMPLIED
+ nohref (nohref) #IMPLIED
+ alt %Text; #REQUIRED
+ target %FrameTarget; #IMPLIED
+ >
+
+<!--================ Forms ===============================================-->
+
+<!ELEMENT form %form.content;> <!-- forms shouldn't be nested -->
+
+<!ATTLIST form
+ %attrs;
+ action %URI; #REQUIRED
+ method (get|post) "get"
+ name NMTOKEN #IMPLIED
+ enctype %ContentType; "application/x-www-form-urlencoded"
+ onsubmit %Script; #IMPLIED
+ onreset %Script; #IMPLIED
+ accept %ContentTypes; #IMPLIED
+ accept-charset %Charsets; #IMPLIED
+ target %FrameTarget; #IMPLIED
+ >
+
+<!--
+ Each label must not contain more than ONE field
+ Label elements shouldn't be nested.
+-->
+<!ELEMENT label %Inline;>
+<!ATTLIST label
+ %attrs;
+ for IDREF #IMPLIED
+ accesskey %Character; #IMPLIED
+ onfocus %Script; #IMPLIED
+ onblur %Script; #IMPLIED
+ >
+
+<!ENTITY % InputType
+ "(text | password | checkbox |
+ radio | submit | reset |
+ file | hidden | image | button)"
+ >
+
+<!-- the name attribute is required for all but submit & reset -->
+
+<!ELEMENT input EMPTY> <!-- form control -->
+<!ATTLIST input
+ %attrs;
+ %focus;
+ type %InputType; "text"
+ name CDATA #IMPLIED
+ value CDATA #IMPLIED
+ checked (checked) #IMPLIED
+ disabled (disabled) #IMPLIED
+ readonly (readonly) #IMPLIED
+ size CDATA #IMPLIED
+ maxlength %Number; #IMPLIED
+ src %URI; #IMPLIED
+ alt CDATA #IMPLIED
+ usemap %URI; #IMPLIED
+ onselect %Script; #IMPLIED
+ onchange %Script; #IMPLIED
+ accept %ContentTypes; #IMPLIED
+ align %ImgAlign; #IMPLIED
+ >
+
+<!ELEMENT select (optgroup|option)+> <!-- option selector -->
+<!ATTLIST select
+ %attrs;
+ name CDATA #IMPLIED
+ size %Number; #IMPLIED
+ multiple (multiple) #IMPLIED
+ disabled (disabled) #IMPLIED
+ tabindex %Number; #IMPLIED
+ onfocus %Script; #IMPLIED
+ onblur %Script; #IMPLIED
+ onchange %Script; #IMPLIED
+ >
+
+<!ELEMENT optgroup (option)+> <!-- option group -->
+<!ATTLIST optgroup
+ %attrs;
+ disabled (disabled) #IMPLIED
+ label %Text; #REQUIRED
+ >
+
+<!ELEMENT option (#PCDATA)> <!-- selectable choice -->
+<!ATTLIST option
+ %attrs;
+ selected (selected) #IMPLIED
+ disabled (disabled) #IMPLIED
+ label %Text; #IMPLIED
+ value CDATA #IMPLIED
+ >
+
+<!ELEMENT textarea (#PCDATA)> <!-- multi-line text field -->
+<!ATTLIST textarea
+ %attrs;
+ %focus;
+ name CDATA #IMPLIED
+ rows %Number; #REQUIRED
+ cols %Number; #REQUIRED
+ disabled (disabled) #IMPLIED
+ readonly (readonly) #IMPLIED
+ onselect %Script; #IMPLIED
+ onchange %Script; #IMPLIED
+ >
+
+<!--
+ The fieldset element is used to group form fields.
+ Only one legend element should occur in the content
+ and if present should only be preceded by whitespace.
+-->
+<!ELEMENT fieldset (#PCDATA | legend | %block; | form | %inline; | %misc;)*>
+<!ATTLIST fieldset
+ %attrs;
+ >
+
+<!ENTITY % LAlign "(top|bottom|left|right)">
+
+<!ELEMENT legend %Inline;> <!-- fieldset label -->
+<!ATTLIST legend
+ %attrs;
+ accesskey %Character; #IMPLIED
+ align %LAlign; #IMPLIED
+ >
+
+<!--
+ Content is %Flow; excluding a, form, form controls, iframe
+-->
+<!ELEMENT button %button.content;> <!-- push button -->
+<!ATTLIST button
+ %attrs;
+ %focus;
+ name CDATA #IMPLIED
+ value CDATA #IMPLIED
+ type (button|submit|reset) "submit"
+ disabled (disabled) #IMPLIED
+ >
+
+<!-- single-line text input control (DEPRECATED) -->
+<!ELEMENT isindex EMPTY>
+<!ATTLIST isindex
+ %coreattrs;
+ %i18n;
+ prompt %Text; #IMPLIED
+ >
+
+<!--======================= Tables =======================================-->
+
+<!-- Derived from IETF HTML table standard, see [RFC1942] -->
+
+<!--
+ The border attribute sets the thickness of the frame around the
+ table. The default units are screen pixels.
+
+ The frame attribute specifies which parts of the frame around
+ the table should be rendered. The values are not the same as
+ CALS to avoid a name clash with the valign attribute.
+-->
+<!ENTITY % TFrame "(void|above|below|hsides|lhs|rhs|vsides|box|border)">
+
+<!--
+ The rules attribute defines which rules to draw between cells:
+
+ If rules is absent then assume:
+ "none" if border is absent or border="0" otherwise "all"
+-->
+
+<!ENTITY % TRules "(none | groups | rows | cols | all)">
+
+<!-- horizontal placement of table relative to document -->
+<!ENTITY % TAlign "(left|center|right)">
+
+<!-- horizontal alignment attributes for cell contents
+
+ char alignment char, e.g. char=':'
+ charoff offset for alignment char
+-->
+<!ENTITY % cellhalign
+ "align (left|center|right|justify|char) #IMPLIED
+ char %Character; #IMPLIED
+ charoff %Length; #IMPLIED"
+ >
+
+<!-- vertical alignment attributes for cell contents -->
+<!ENTITY % cellvalign
+ "valign (top|middle|bottom|baseline) #IMPLIED"
+ >
+
+<!ELEMENT table
+ (caption?, (col*|colgroup*), thead?, tfoot?, (tbody+|tr+))>
+<!ELEMENT caption %Inline;>
+<!ELEMENT thead (tr)+>
+<!ELEMENT tfoot (tr)+>
+<!ELEMENT tbody (tr)+>
+<!ELEMENT colgroup (col)*>
+<!ELEMENT col EMPTY>
+<!ELEMENT tr (th|td)+>
+<!ELEMENT th %Flow;>
+<!ELEMENT td %Flow;>
+
+<!ATTLIST table
+ %attrs;
+ summary %Text; #IMPLIED
+ width %Length; #IMPLIED
+ border %Pixels; #IMPLIED
+ frame %TFrame; #IMPLIED
+ rules %TRules; #IMPLIED
+ cellspacing %Length; #IMPLIED
+ cellpadding %Length; #IMPLIED
+ align %TAlign; #IMPLIED
+ bgcolor %Color; #IMPLIED
+ >
+
+<!ENTITY % CAlign "(top|bottom|left|right)">
+
+<!ATTLIST caption
+ %attrs;
+ align %CAlign; #IMPLIED
+ >
+
+<!--
+colgroup groups a set of col elements. It allows you to group
+several semantically related columns together.
+-->
+<!ATTLIST colgroup
+ %attrs;
+ span %Number; "1"
+ width %MultiLength; #IMPLIED
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!--
+ col elements define the alignment properties for cells in
+ one or more columns.
+
+ The width attribute specifies the width of the columns, e.g.
+
+ width=64 width in screen pixels
+ width=0.5* relative width of 0.5
+
+ The span attribute causes the attributes of one
+ col element to apply to more than one column.
+-->
+<!ATTLIST col
+ %attrs;
+ span %Number; "1"
+ width %MultiLength; #IMPLIED
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!--
+ Use thead to duplicate headers when breaking table
+ across page boundaries, or for static headers when
+ tbody sections are rendered in scrolling panel.
+
+ Use tfoot to duplicate footers when breaking table
+ across page boundaries, or for static footers when
+ tbody sections are rendered in scrolling panel.
+
+ Use multiple tbody sections when rules are needed
+ between groups of table rows.
+-->
+<!ATTLIST thead
+ %attrs;
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!ATTLIST tfoot
+ %attrs;
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!ATTLIST tbody
+ %attrs;
+ %cellhalign;
+ %cellvalign;
+ >
+
+<!ATTLIST tr
+ %attrs;
+ %cellhalign;
+ %cellvalign;
+ bgcolor %Color; #IMPLIED
+ >
+
+<!-- Scope is simpler than headers attribute for common tables -->
+<!ENTITY % Scope "(row|col|rowgroup|colgroup)">
+
+<!-- th is for headers, td for data and for cells acting as both -->
+
+<!ATTLIST th
+ %attrs;
+ abbr %Text; #IMPLIED
+ axis CDATA #IMPLIED
+ headers IDREFS #IMPLIED
+ scope %Scope; #IMPLIED
+ rowspan %Number; "1"
+ colspan %Number; "1"
+ %cellhalign;
+ %cellvalign;
+ nowrap (nowrap) #IMPLIED
+ bgcolor %Color; #IMPLIED
+ width %Length; #IMPLIED
+ height %Length; #IMPLIED
+ >
+
+<!ATTLIST td
+ %attrs;
+ abbr %Text; #IMPLIED
+ axis CDATA #IMPLIED
+ headers IDREFS #IMPLIED
+ scope %Scope; #IMPLIED
+ rowspan %Number; "1"
+ colspan %Number; "1"
+ %cellhalign;
+ %cellvalign;
+ nowrap (nowrap) #IMPLIED
+ bgcolor %Color; #IMPLIED
+ width %Length; #IMPLIED
+ height %Length; #IMPLIED
+ >
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/faq.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,271 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Isabelle FAQ</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="main">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation.include.html"?>
+ <div class="hr"><hr/></div>
+ <div id="content">
+
+ <h2>General Questions</h2>
+
+ <dl class="faq">
+
+ <dt>What is Isabelle?</dt>
+
+ <dd>Isabelle is a popular generic theorem proving environment developed
+ at Cambridge University (<a href=
+ "http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU Munich
+ (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>). See the
+ <a href="http://isabelle.in.tum.de/">Isabelle homepage</a> for more
+ information.</dd>
+
+ <dt>Where can I find documentation?</dt>
+
+ <dd><a href="http://isabelle.in.tum.de/docs.html">This way, please</a>.
+ Also have a look at the <a href=
+ "http://isabelle.in.tum.de/library/">theory library</a>.</dd>
+
+ <dt>Is it available for download?</dt>
+
+ <dd>Yes, it is available from <a href=
+ "http://isabelle.in.tum.de/dist/">several mirror sites</a>. It should run
+ on most recent Unix systems (Solaris, Linux, MacOS X, etc.).</dd>
+
+</dl>
+ <h2>Syntax</h2>
+
+ <dl class="faq">
+
+ <dt>There are lots of arrows in Isabelle. What's the difference between
+ <tt>-></tt>, <tt>=></tt>, <tt>--></tt>, and <tt>==></tt>
+ ?</dt>
+
+ <dd>Isabelle uses the <tt>=></tt> arrow for the function type
+ (contrary to most functional languages which use <tt>-></tt>). So
+ <tt>a => b</tt> is the type of a function that takes an element of
+ <tt>a</tt> as input and gives you an element of <tt>b</tt> as output. The
+ long arrow <tt>--></tt> and <tt>==></tt> are object and meta level
+ implication. Roughly speaking, the meta level implication should only be
+ used when stating theorems where it separates the assumptions from the
+ conclusion. Whenever you need an implication inside a HOL formula, use
+ <code>--></code>.</dd>
+
+ <dt>Where do I have to put those double quotes?</dt>
+
+ <dd>Isabelle distinguishes between <em>inner</em> and <em>outer</em>
+ syntax. The outer syntax comes from the Isabelle framework, the inner
+ syntax is the one in between quotation marks and comes from the object
+ logic (in this case HOL). With time the distinction between the two
+ becomes obvious, but in the beginning the following rules of thumb may
+ work: types should be inside quotation marks, formulas and lemmas should
+ be inside quotation marks, rules and equations (e.g. for definitions)
+ should be inside quotation marks, commands like <tt>lemma</tt>,
+ <tt>consts</tt>, <tt>primrec</tt>, <tt>constdefs</tt>, <tt>apply</tt>,
+ <tt>done</tt> are without quotation marks, as are the names of constants
+ in constant definitions (<tt>consts</tt> and <tt>constdefs</tt>)</dd>
+
+ <dt>What is <tt>"No such constant: _case_syntax"</tt> supposed to tell
+ me?</dt>
+
+ <dd>You get this message if you use a case construct on a datatype and
+ have a typo in the names of the constructor patterns or if the order of
+ the constructors in the case pattern is different from the order in which
+ they where defined (in the datatype definition).</dd>
+
+ <dt>Why doesn't Isabelle understand my equation?</dt>
+
+ <dd>Isabelle's equality <tt>=</tt> binds relatively strongly, so an
+ equation like <tt>a = b & c</tt> might not be what you intend.
+ Isabelle parses it as <tt>(a = b) & c</tt>. If you want it the other
+ way around, you must set explicit parentheses as in <tt>a = (b &
+ c)</tt>. This also applies to e.g. <tt>primrec</tt> definitions (see
+ below).</dd>
+
+ <dt>What does it mean "not a proper equation"?</dt>
+
+ <dd>Most commonly this is an instance of the question above. The
+ <tt>primrec</tt> command (and others) expect equations as input, and
+ since equality binds strongly in Isabelle, something like <tt>f x = b
+ & c</tt> is not what you might expect it to be: Isabelle parses it as
+ <tt>(f x = b) & c</tt> (which is indeed not a proper equation). To
+ turn it into an equation you must set explicit parentheses: <tt>f x = (b
+ & c)</tt>.</dd>
+
+ <dt>What does it mean "<tt>Not a meta-equality (==)</tt>"?</dt>
+
+ <dd>This usually occurs if you use <tt>=</tt> for <tt>constdefs</tt>. The
+ <tt>constdefs</tt> and <tt>defs</tt> commands expect not equations, but
+ meta equivalences. Just use the <tt>\<equiv></tt> or <tt>==</tt>
+ signs instead of <tt>=</tt>.</dd>
+
+</dl>
+ <h2>Proving</h2>
+
+ <dl class="faq">
+
+ <dt>What does "empty result sequence" mean?</dt>
+
+ <dd>It means that the applied proof method (or tactic) was unsuccessful.
+ It did not transform the goal in any way, or simply just failed to do
+ anything. You must try another tactic (or give the one you used more
+ hints or lemmas to work with)</dd>
+
+ <dt>The Simplifier doesn't want to apply my rule, what's wrong?</dt>
+
+ <dd>Most commonly this is a typing problem. The rule you want to apply
+ may require a more special (or just plain different) type from what you
+ have in the current goal. Use the ProofGeneral menu <tt>Isabelle/Isar
+ -> Settings -> Show Types</tt> and the <tt>thm</tt> command on the
+ rule you want to apply to find out if the types are what you expect them
+ to be (also take a look at the types in your goal). <tt>Show Sorts</tt>,
+ <tt>Show Constants</tt>, and <tt>Trace Simplifier</tt> in the same menu
+ may also be helpful.</dd>
+
+ <dt>If I do <tt>auto</tt>, it leaves me a goal <tt>False</tt>. Is my
+ theorem wrong?</dt>
+
+ <dd>Not necessarily. It just means that <tt>auto</tt> transformed the
+ goal into something that is not provable any more. That could be due to
+ <tt>auto</tt> doing something stupid, or e.g. due to some earlier step in
+ the proof that lost important information. It is of course also possible
+ that the goal was never provable in the first place.</dd>
+
+ <dt>Why does <tt>lemma "1+1=2"</tt> fail?</dt>
+
+ <dd>Because it is not necessarily true. Isabelle does not assume that 1
+ and 2 are natural numbers. Try <tt>"(1::nat)+1=2"</tt> instead.</dd>
+
+ <dt>Can Isabelle find counterexamples?</dt>
+
+ <dd>
+ <p>For arithmetic goals, <code>arith</code> finds counterexamples. For
+ executable goals, <code>quickcheck</code> tries to find a
+ counterexample. For goals of a more logical nature (including
+ quantifiers, sets and inductive definitions) <code>refute</code>
+ searches for a countermodel.</p>
+
+ <p>Otherwise, negate the proposition and instantiate (some) variables
+ with concrete values. You may also need additional assumptions about
+ these values. For example, <tt>True & False ~= True | False</tt> is
+ a counterexample of <tt>A & B = A | B</tt>, and <tt>A = ~B ==> A
+ & B ~= A | B</tt> is another one. Sometimes Isabelle can help you
+ to find the counterexample: just negate the proposition and do
+ <tt>auto</tt> or <tt>simp</tt>. If lucky, you are left with the
+ assumptions you need for the counterexample to work.</p>
+ </dd>
+
+</dl>
+ <h2>Interface</h2>
+
+ <dl class="faq">
+
+ <dt>ProofGeneral appears to hang when Isabelle is started.</dt>
+ <dd><p>This may be because of UTF-8 issues e.g. in Red Hat 8.0/9.0, Suse
+ 9.0/9.1</p>
+ <p>RedHat 8 and later has glibc 2.2 and UTF8 encoded output may be turned on
+ in default locale. Unfortunately Proof General relies on 8-bit characters
+ which are UTF8 prefixes in the output of proof assistants (inc Coq,
+ Isabelle). These prefix characters are not flushed to stdout individually. As
+ a workaround we must find a way to disable interpretation of UTF8 in the C
+ libraries that Coq and friends use.</p>
+
+ <p>Doing this inside PG/Emacs seems tricky; locale settings are set/inherited
+ in strange ways. One solution is to run the Emacs process itself with an
+ altered locale setting, for example, starting XEmacs by typing:</p>
+
+ <p><tt>$ LC_CTYPE=en_GB Isabelle &</tt></p>
+
+ <p>The supplied proofgeneral script makes this setting if it sees the string
+ UTF in the current value of LC_CTYPE. Depending on your distribution, this
+ variable might also be called <tt>LANG</tt>.</p>
+
+ <p>Alternatively you can set LC_CTYPE or LANG inside a file ~/.i18n, which
+ will be read by the shell. This will affect all applications, though. [
+ suggestions for a better workaround inside Emacs would be welcome ]</p>
+
+ <p>NB: a related issue is warnings from x-symbol: "Emacs language environment
+ and system locale specify different encoding, I'll assume `iso-8859-1'". This
+ warning appears to be mainly harmless. Notice that the variable
+ `buffer-file-coding-system' may determine the format that files are saved
+ in.</p></dd>
+
+ <dt>X-Symbol doesn't seem to work. What can I do?</dt>
+
+ <dd>The most common reason why X-Symbol doesn't work is: it's not
+ switched on yet. Assuming you are using ProofGeneral and have installed
+ the X-Symbol package, you still need to turn X-Symbol on in ProofGeneral:
+ select the menu items <tt>Proof-General -> Options -> X-Symbol</tt>
+ and (if you want to save the setting for future sessions) select
+ <tt>Options -> Save Options</tt> in XEmacs.</dd>
+
+ <dt>How do I input those X-Symbols anyway?</dt>
+
+ <dd>There are lots of ways to input x-symbols. The one that always works
+ is writing it out in plain text (e.g. for the 'and' symbol type
+ <tt>\<and></tt>). For common symbols you can try to "paint them in
+ ASCII" and if the xsymbol package recognizes them it will automatically
+ convert them into their graphical representation. Examples:
+ <tt>--></tt> is converted into the long single arrow, <tt>/\</tt> is
+ converted into the 'and' symbol, the sequence <tt>=_</tt> into the
+ equivalence sign, <tt><_</tt> into less-or-equal, <tt>[|</tt> into
+ opening semantic brackets, and so on. For greek characters, the
+ <code>rotate</code> command works well: to input α type
+ <code>a</code> and then <code>C-.</code> (control and <code>.</code>).
+ You can also display the grid-of-characters in the x-symbol menu to get
+ an overview of the available graphical representations (not all of them
+ already have a meaning in Isabelle, though).</dd>
+
+</dl>
+ <h2>System</h2>
+
+ <dl class="faq">
+
+ <dt>I want to generate one of those flashy LaTeX documents. How?</dt>
+
+ <dd>You will need to work with the <tt>isatool</tt> command for this (in
+ a Unix shell). The easiest way to get to a document is the following: use
+ <tt>isatool mkdir</tt> to set up a new directory. The command will also
+ create a file called <tt>IsaMakefile</tt> in the current directory. Put
+ your theory file(s) into the new directory and edit the file
+ <tt>ROOT.ML</tt> in there (following the comments) to tell Isabelle which
+ of the theories to load (and in which order). Go back to the parent
+ directory (where the <tt>IsaMakefile</tt> is) and type <tt>isatool
+ make</tt>. Isabelle should then process your theories and tell you where
+ to find the finished document. For more information on generating
+ documents see the Isabelle Tutorial, Chapter 4.</dd>
+
+ <dt>I have a large formalization with many theories. Must I process all
+ of them all of the time?</dt>
+
+ <dd>No, you can tell Isabelle to build a so-called heap image. This heap
+ image can contain your preloaded theories. To get one, set up a directory
+ with a <tt>ROOT.ML</tt> file (as for generating a document) and use the
+ command <tt>isatool usedir -b HOL MyImage</tt> in that directory to
+ create an image <tt>MyImage</tt> using the parent logic <tt>HOL</tt>. You
+ should then be able to invoke Isabelle with <tt>Isabelle -l MyImage</tt>
+ and have everything that is loaded in ROOT.ML instantly available.</dd>
+
+ <dt>Does Isabelle run on Windows?</dt>
+
+ <dd>After a fashion, yes, but Isabelle is not being developed for
+ Windows. See the <a href="dist/installation_notes_cygwin.html">installation notes</a> for windows.
+ If the approach presented there is not sufficient for your purpose, consider a
+ dualboot Windows/Linux system.</dd>
+
+ </dl>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="//include/footer.include.html"?>
+</body>
+
+</html>
Binary file Admin/website/img/c_isabelle_lemmas.gif has changed
Binary file Admin/website/img/isabelle.gif has changed
Binary file Admin/website/img/isabelle_pg_screenshot_big.png has changed
Binary file Admin/website/img/isabelle_pg_screenshot_small.png has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/include/documentationdist.include.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,27 @@
+<?xml version="1.0" encoding="iso-8859-1" ?>
+<dummy:wrapper xmlns:dummy="http://nowhere.no">
+<h3>Learning Isabelle</h3>
+<ul>
+ <li><a target='_blank' href='//dist/packages/Isabelle/doc/tutorial.pdf'>Tutorial on Isabelle/HOL</a></li>
+ <li><a target='_blank' href='//dist/packages/Isabelle/doc/isar-overview.pdf'>Tutorial on Isar</a></li>
+ <li><a target='_blank' href='//dist/packages/Isabelle/doc/locales.pdf'>Tutorial on Locales</a></li>
+</ul>
+<h3>Reference Manuals</h3>
+<ul>
+ <li><a target='_blank' href='//dist/packages/Isabelle/doc/isar-ref.pdf'>The Isabelle/Isar Reference Manual</a></li>
+ <li><a target='_blank' href='//dist/packages/Isabelle/doc/ref.pdf'>The Isabelle Reference Manual</a></li>
+ <li><a target='_blank' href='//dist/packages/Isabelle/doc/system.pdf'>The Isabelle System Manual</a></li>
+</ul>
+<h3>Logics</h3>
+<ul>
+ <li><a target='_blank' href='//dist/packages/Isabelle/doc/logics.pdf'>Isabelle's Logics: overview and misc logics</a></li>
+ <li><a target='_blank' href='//dist/packages/Isabelle/doc/logics-HOL.pdf'>Isabelle's Logics: HOL</a></li>
+ <li><a target='_blank' href='//dist/packages/Isabelle/doc/logics-ZF.pdf'>Isabelle's Logics: FOL and ZF</a></li>
+</ul>
+<h3>Specific Topics</h3>
+<ul>
+ <li><a target='_blank' href='//dist/packages/Isabelle/doc/sugar.pdf'>LaTeX sugar for proof documents</a></li>
+ <li><a target='_blank' href='//dist/packages/Isabelle/doc/axclass.pdf'>Tutorial on Axiomatic Type Classes</a></li>
+ <li><a target='_blank' href='//dist/packages/Isabelle/doc/ind-defs.pdf'>(Co)Inductive Definitions in ZF</a></li>
+</ul>
+</dummy:wrapper>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/include/downloadtable.include.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,117 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE table PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<table class="download">
+ <tr><td colspan="3" class="downloadheader">Isabelle</td></tr>
+ <tr>
+ <td>
+ Sources and documentation
+ </td>
+ <?downloadCells target="//dist/packages/Isabelle2004.tar.gz" title="Isabelle2004.tar.gz"?>
+ </tr>
+ <tr>
+ <td>
+ Documentation in PDF
+ </td>
+ <?downloadCells target="//dist/packages/Isabelle2004_pdf.tar.gz" title="Isabelle2004_pdf.tar.gz"?>
+ </tr>
+ <tr>
+ <td>
+ Theory library in PDF and HTML
+ </td>
+ <?downloadCells target="//dist/packages/Isabelle2004_library.tar.gz" title="Isabelle2004_library.tar.gz"?>
+ </tr>
+ <tr><td colspan="3" class="downloadheader">Proof General</td></tr>
+ <tr>
+ <td>
+ Proof General
+ </td>
+ <?downloadCells target="//dist/packages/contrib/ProofGeneral-3.5.tar.gz" title="ProofGeneral-3.5.tar.gz"?>
+ </tr>
+ <tr><td colspan="3" class="downloadheader">Poly/ML compiler and runtime system</td></tr>
+ <tr>
+ <td>
+ Poly/ML base system
+ </td>
+ <?downloadCells target="//dist/packages/contrib/polyml_base.tar.gz" title="polyml_base.tar.gz"?>
+ </tr>
+ <tr>
+ <td rowspan="3">
+ Poly/ML binary modules
+ </td>
+ <?downloadCells target="//dist/packages/contrib/polyml_x86-linux.tar.gz" title="polyml_x86-linux.tar.gz"?>
+ </tr>
+ <tr>
+ <td style="display: none"></td>
+ <?downloadCells target="//dist/packages/contrib/polyml_sparc-solaris.tar.gz" title="polyml_sparc-solaris.tar.gz"?>
+ </tr>
+ <tr>
+ <td style="display: none"></td>
+ <?downloadCells target="//dist/packages/contrib/polyml_ppc-darwin.tar.gz" title="polyml_ppc-darwin.tar.gz"?>
+ </tr>
+ <tr><td colspan="3" class="downloadheader">Precompiled logics</td></tr>
+ <tr>
+ <td rowspan="3">
+ HOL
+ </td>
+ <?downloadCells target="//dist/packages/HOL_x86-linux.tar.gz" title="HOL_x86-linux.tar.gz"?>
+ </tr>
+ <tr>
+ <td style="display: none"></td>
+ <?downloadCells target="//dist/packages/HOL_sparc-solaris.tar.gz" title="HOL_sparc-solaris.tar.gz"?>
+ </tr>
+ <tr>
+ <td style="display: none"></td>
+ <?downloadCells target="//dist/packages/HOL_ppc-darwin.tar.gz" title="HOL_ppc-darwin.tar.gz"?>
+ </tr>
+ <tr>
+ <td rowspan="3">
+ HOL-Complex
+ </td>
+ <?downloadCells target="//dist/packages/HOL-Complex_x86-linux.tar.gz" title="HOL-Complex_x86-linux.tar.gz"?>
+ </tr>
+ <tr>
+ <td style="display: none"></td>
+ <?downloadCells target="//dist/packages/HOL-Complex_sparc-solaris.tar.gz" title="HOL-Complex_sparc-solaris.tar.gz"?>
+ </tr>
+ <tr>
+ <td style="display: none"></td>
+ <?downloadCells target="//dist/packages/HOL-Complex_ppc-darwin.tar.gz" title="HOL-Complex_ppc-darwin.tar.gz"?>
+ </tr>
+ <tr>
+ <td rowspan="3">
+ HOL4
+ </td>
+ <?downloadCells target="//dist/packages/HOL4_x86-linux.tar.gz" title="HOL4_x86-linux.tar.gz"?>
+ </tr>
+ <tr>
+ <td style="display: none"></td>
+ <?downloadCells target="//dist/packages/HOL4_sparc-solaris.tar.gz" title="HOL4_sparc-solaris.tar.gz"?>
+ </tr>
+ <tr>
+ <td style="display: none"></td>
+ <?downloadCells target="//dist/packages/HOL4_ppc-darwin.tar.gz" title="HOL4_ppc-darwin.tar.gz"?>
+ </tr>
+ <tr>
+ <td rowspan="3">
+ ZF
+ </td>
+ <?downloadCells target="//dist/packages/ZF_x86-linux.tar.gz" title="ZF_x86-linux.tar.gz"?>
+ </tr>
+ <tr>
+ <td style="display: none"></td>
+ <?downloadCells target="//dist/packages/ZF_sparc-solaris.tar.gz" title="ZF_sparc-solaris.tar.gz"?>
+ </tr>
+ <tr>
+ <td style="display: none"></td>
+ <?downloadCells target="//dist/packages/ZF_ppc-darwin.tar.gz" title="ZF_ppc-darwin.tar.gz"?>
+ </tr>
+ <tr><td colspan="3" class="downloadheader">HOL4 proof terms</td></tr>
+ <tr>
+ <td>
+ HOL4 proof terms
+ </td>
+ <?downloadCells target="//dist/packages/contrib/HOL4-proofs.tar.gz" title="HOL4-proofs.tar.gz"?>
+</tr>
+</table>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/include/footer.include.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,6 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE div PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<div id="footer">
+ <p>Last updated: <?modificationDate?></p>
+</div>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/include/header.include.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,17 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE div PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<div id="header">
+ <h1><?title?></h1>
+ <a id="isabelle_logo" href="http://isabelle.in.tum.de/index.html">
+ <img src="//dist/img/isabelle_logo.gif" width="114" height="100" alt="Isabelle home" />
+ </a>
+ <span class="headersep">·</span>
+ <a id="univ_tum" target="_blank" href="http://www4.in.tum.de/proj/theoremprov/group.html">
+ <img src="//dist/img/univ_tum.gif" width="45" height="55" alt="Isabelle in Munich" />
+ </a>
+ <span class="headersep">·</span>
+ <a id="univ_cambridge" target="_blank" href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html">
+ <img src="//dist/img/univ_cambridge.gif" width="169" height="55" alt="Isabelle in Cambridge" />
+ </a>
+</div>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/include/htmlheader.include.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,15 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<dummy:wrapper xmlns:dummy="http://nowhere.no">
+ <?contentType?>
+ <link rel="stylesheet" type="text/css" media="all" href="//dist/css/aelfwine.css"/>
+ <link rel="stylesheet" type="text/css" media="all" href="//dist/css/isabelle_base.css"/>
+ <style type="text/css" media="screen">
+ @import url(<?relativeRoot href="dist/css/isabelle_screen.css"?>);
+ </style>
+ <link rel="stylesheet" type="text/css" media="print" href="//dist/css/isabelle_print.css"/>
+ <link rel="icon" href="//dist/img/favicon.ico" type="image/icon"/>
+ <meta name="language" content="en"/>
+ <meta name="robots" content="index follow"/>
+</dummy:wrapper>
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/include/navigation.include.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,13 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE div PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<div id="navigation">
+ <h2>Navigation</h2>
+ <ul>
+ <?navitem target="index.html" title="Home" ?>
+ <?navitem target="overview.html" title="Overview" ?>
+ <?navitem target="logics.html" title="Logics" ?>
+ <?navitem target="community.html" title="Community" ?>
+ <?navitem target="dist/index.html" title="Distribution" ?>
+ </ul>
+</div>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/include/navigation_dist.include.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,13 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE div PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<div id="navigation">
+ <h2>Navigation</h2>
+ <ul>
+ <?navitem target="index.html" title="Mirrors" ?>
+ <?navitem target="installation.html" title="Installation" ?>
+ <?navitem target="download.html" title="Download" ?>
+ <?navitem target="documentation.html" title="Documentation" ?>
+ <?navitem target="others.html" title="Other links" ?>
+ </ul>
+</div>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/index.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,124 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Isabelle</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="main">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation.include.html"?>
+ <div class="hr"><hr/></div>
+ <div id="content">
+ <h2>What is Isabelle?</h2>
+ <p>
+ Isabelle is a popular generic theorem proving environment
+ developed at Cambridge University (<a
+ href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>)
+ and TU Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias
+ Nipkow</a>). See the <a href="overview.html">Isabelle
+ overview</a>.
+ </p>
+ <p>
+ These pages provide general information on Isabelle, more
+ specific information is available from the local pages
+ </p>
+
+ <ul>
+
+ <li><a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle
+ at Cambridge</strong></a></li>
+
+ <li><a href="http://www4.in.tum.de/proj/theoremprov/group.html"><strong>Isabelle
+ at Munich</strong></a></li>
+
+ </ul>
+
+ <p>
+ See there for information on projects done with Isabelle,
+ mailing list archives, research papers, the Isabelle
+ bibliography, and Isabelle workshops and courses.
+ </p>
+
+
+ <h2>Coming soon: Isabelle 2005</h2>
+ <p>New features in the upcoming Isabelle 2005 will include</p>
+ <ul>
+ <li>New commands for instantiating locales</li>
+ <li>New command for finding matching rewrite rules</li>
+ <li>Finding theorems by term patterns</li>
+ <li>New automatic transitivity reasoner</li>
+ <li>New command for ad-hoc theory viewing and printing</li>
+ <li>Much extended and improved theory of finite sets</li>
+ <li>New syntax that will allow > and >= in addition to < and
+ <=</li>
+ </ul>
+
+ <h2>Isabelle 2004</h2>
+
+<p>New features in Isabelle 2004 include</p>
+
+<ul>
+<li>New image HOL4 with imported library from HOL4 system on top of
+ HOL-Complex (about 2500 additional theorems).</li>
+
+<li>New theory Ring_and_Field with over 250 basic numerical laws,
+ all proved in axiomatic type classes for semirings, rings and fields.</li>
+
+<li>New locale <code>ring</code> for non-commutative rings in HOL-Algebra.</li>
+
+<li>Type <code>rat</code> of the rational numbers available in HOL-Complex.</li>
+
+<li>New theory of matrices with an application to linear programming in HOL-Matrix.</li>
+
+<li>Improved locales (named proof contexts), instantiation of locales.</li>
+
+<li>Improved handling of linear and partial orders in simplifier.</li>
+
+<li>New <code>specification</code> command for definition by specification.</li>
+
+<li>New Isar command <code>finalconsts</code> prevents constants being given a definition later.</li>
+
+<li><code>arith</code> now generates counterexamples for reals as well.</li>
+
+<li>New <code>quickcheck</code> command
+ to search for counterexamples of executable goals.
+ (see HOL/ex/Quickcheck_Examples.thy)</li>
+<li>New <code>refute</code> command
+ to search for finite countermodels of goals.
+ (see HOL/ex/Refute_Examples.thy)
+</li>
+
+<li>Presentation and x-symbol enhancements, greek letters and
+sub/superscripts allowed in identifiers.</li>
+</ul>
+
+<p><a href="isabelle/Isabelle/NEWS">[Complete Changelog]</a></p>
+
+<h2>Download</h2>
+
+<p>
+The Isabelle distribution is available
+from several <a href="dist/index.html">mirror sites</a>. It includes
+source and binary packages and browsable documentation. You can also
+browse the <a href="library/index.html">Isabelle theory library</a>
+online.
+</p>
+
+<p>
+Use the mailing list <a
+href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
+and its <a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to
+discuss problems and results. To subscribe, <a href="mailto:lcp@cl.cam.ac.uk?subject=subscribe&body=Please%20add%20me%20to%20the%20Isabelle%20mailing%20list">contact Larry Paulson</a>.
+</p>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="//include/footer.include.html"?>
+</body>
+
+</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/logics.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,103 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Logics</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="main">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation.include.html"?>
+ <div class="hr"><hr/></div>
+ <div id="content">
+ <h2>Isabelle's Logics</h2>
+ <p>Isabelle can be viewed from two main
+ perspectives. On the one hand it may serve as a generic framework for rapid
+ prototyping of deductive systems. On the other hand, major existing logics
+ like <a href="#isabelle_hol"><em>Isabelle/HOL</em></a>
+ provide a theorem proving environment
+ ready to use for sizable applications.</p>
+
+ <p>The Isabelle distribution includes a large body of
+ object logics and other examples (see the <a href=
+ "library/index.html">Isabelle theory library</a>).</p>
+
+ <dl>
+ <dt id="isabelle_hol"><a href="library/HOL/index.html">Isabelle/HOL</a></dt>
+ <dd>is a version of classical higher-order logic resembling that of the
+ <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>. The
+ main libraries of the HOL 4 System are now <a href=
+ "library/HOL/HOL-Complex/HOL4/index.html">available in Isabelle</a>.</dd>
+
+ <dt><a href=
+ "library/HOLCF/index.html">Isabelle/HOLCF</a></dt>
+ <dd>adds Scott's Logic for Computable Functions (domain theory) to
+ HOL.</dd>
+
+ <dt><a href="library/FOL/index.html">Isabelle/FOL</a></dt>
+ <dd>provides basic classical and intuitionistic first-order logic. It is
+ polymorphic.</dd>
+
+ <dt><a href="library/ZF/index.html">Isabelle/ZF</a></dt>
+ <dd>offers a formulation of Zermelo-Fraenkel set theory on top of FOL.</dd>
+ </dl>
+
+ <p><em>Isabelle/HOL</em> is currently the best developed object logic, including an
+ extensive library of (concrete) mathematics, and various packages for
+ advanced definitional concepts like (co-)inductive sets and types,
+ well-founded recursion etc. The distribution also includes some large
+ applications, for example correctness proofs of cryptographic protocols
+ (<a href="library/HOL/Auth/index.html">HOL/Auth</a>) or communication
+ protocols (<a href="library/HOLCF/IOA/index.html">HOLCF/IOA</a>).</p>
+
+ <p><em>Isabelle/ZF</em> provides another starting point for applications, with a
+ slightly less developed library. Its definitional packages are similar to
+ those of Isabelle/HOL. Untyped ZF provides more advanced constructions for
+ sets than simply-typed HOL.</p>
+
+ <p>There are a few minor object logics that may serve as further examples:
+ <a href="library/CTT/index.html">CTT</a> is an extensional version of
+ Martin-Löf's Type Theory, <a href="library/Cube/index.html">Cube</a> is
+ Barendregt's Lambda Cube. There are also some sequent calculus examples under
+ <a href="library/Sequents/index.html">Sequents</a>, including modal and
+ linear logics. Again see the <a href="library/index.html">Isabelle theory
+ library</a> for other examples.</p>
+
+ <h2>Defining Logics</h2>
+
+ <p>Logics are not hard-wired into Isabelle, but
+ formulated within Isabelle's meta logic: <em>Isabelle/Pure</em>.
+ There are quite a lot of syntactic and deductive tools available in generic
+ Isabelle. Thus defining new logics or extending existing ones basically works
+ as follows:</p>
+
+ <ol>
+ <li>declare concrete syntax (via mixfix grammar and syntax macros)</li>
+ <li>declare abstract syntax (as higher-order constants)</li>
+ <li>declare inference rules (as meta-logical propositions)</li>
+ <li>instantiate generic automatic proof tools (simplifier, classical
+ tableau prover etc.)</li>
+ <li>manually code special proof procedures (via tacticals or hand-written
+ ML)</li>
+ </ol>
+
+ <p>The first three steps above are fully declarative and involve no ML
+ programming at all. Thus one already gets a decent deductive environment
+ based on primitive inferences (by employing the built-in mechanisms of
+ <em>Isabelle/Pure</em>, in particular higher-order unification and resolution). For
+ sizable applications some degree of automated reasoning is essential.
+ Instantiating existing tools like the classical tableau prover involves only
+ minimal ML-based setup. One may also write arbitrary proof procedures or even
+ theory extension packages in ML, without breaching system soundness (Isabelle
+ follows the well-known <em>LCF system approach</em> to achieve a secure
+ system).</p>
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="//include/footer.include.html"?>
+</body>
+
+</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/makefile Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,5 @@
+# isaweb makefile
+# $Id$
+
+# just delegate
+include build/main.mak
Binary file Admin/website/media/pg_preview.pdf has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/overview.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,106 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<?cvs id="$Id$"?>
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+ <title>Overview</title>
+ <?include file="//include/htmlheader.include.html"?>
+</head>
+
+<body class="main">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation.include.html"?>
+ <div class="hr"><hr/></div>
+ <div id="content">
+ <h2>What is Isabelle?</h2>
+ <p>
+ Isabelle is a generic proof assistant. It allows mathematical
+ formulas to be expressed in a formal language and provides tools
+ for proving those formulas in a logical calculus. The main
+ application is the formalization of mathematical proofs and in
+ particular <em>formal verification</em>, which includes proving
+ the correctness of computer hardware or software and proving
+ properties of computer languages and protocols.</p>
+
+ <p>Compared with similar tools, Isabelle's distinguishing feature is its
+ flexibility. Most proof assistants are built around a single formal calculus,
+ typically higher-order logic. Isabelle has the capacity to accept a variety
+ of formal calculi. The distributed version supports higher-order logic but
+ also axiomatic set theory and several other formalisms. See
+ <a href="logics.html">logics</a> for more details.</p>
+
+ <p>Isabelle is a joint project between Lawrence C. Paulson
+ (University of Cambridge, UK) and Tobias Nipkow (Technical
+ University of Munich, Germany).</p>
+
+ <h2>What Isabelle offers</h2>
+
+ <a href="//img/isabelle_pg_screenshot_big.png">
+ <img class="left" src="//img/isabelle_pg_screenshot_small.png" alt="Sreenshot "
+ width="250" height="277" />
+ </a>
+
+ <p>Isabelle provides excellent notational support: new notations
+ can be introduced, using normal mathematical symbols. Proofs can
+ be written in a structured notation based upon traditional proof
+ style, or more straightforwardly as sequences of
+ commands. Definitions and proofs may include TeX source, from
+ which Isabelle can automatically generate typeset documents.</p>
+
+ <p>The main limitation of all such proof systems is that proving
+ theorems requires much effort from an expert user. Isabelle
+ incorporates some tools to improve the user's productivity by
+ automating some parts of the proof process. In particular,
+ Isabelle's <em>classical reasoner</em> can perform long chains
+ of reasoning steps to prove formulas. The <em>simplifier</em>
+ can reason with and about equations. Linear <em>arithmetic</em>
+ facts are proved automatically.</p>
+
+ <p>Isabelle comes with a large theory library of formally
+ verified mathematics, including elementary number theory (for
+ example, Gauss's law of quadratic reciprocity), analysis (basic
+ properties of limits, derivatives and integrals), algebra (up to
+ Sylow's theorem) and set theory (the relative consistency of the
+ Axiom of Choice). Also provided are numerous examples arising
+ from research into formal verification.</p>
+
+ <p>With <em>Isar</em>, Isabelle offers a concise proof formulation language
+ which enables a user to write proof scripts naturally understandable for
+ both humans <em>and</em> computers.</p>
+
+ <p>Isabelle is closely integrated with the <a href=
+ "http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> user interface, which
+ eases the task of writing and maintaining proof scripts.</p>
+ <br clear="both" />
+
+ <h2>Preview</h2>
+
+ <p>We provide a <a href="PG-preview.mov">hyperlinked preview</a> demonstrating
+ Isabelle and ProofGeneral, in <a href="http://www.apple.com/quicktime/download/">QuickTime
+ format</a>, and also as a <a href="PG-preview.pdf">non-hyperlinked preview</a> in PDF.</p>
+
+ <p>Ample <a href="dist/documentation.html">documentation</a> is available
+ about using Isabelle and its inner concepts, including a
+ <a href="http://www4.in.tum.de/~nipkow/LNCS2283/">Tutorial</a> published by
+ Springer-Verlag.</p>
+
+ <h2>Projects</h2>
+
+ <p>There is an (incomplete) list of past and present <a href=
+ "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/projects.html">projects</a>
+ undertaken using Isabelle available.</p>
+
+ <h2>License</h2>
+
+ <p>Isabelle is distributed free of charge under the open source
+ <a href="dist/Isabelle/COPYRIGHT">BSD license</a>. You may use any of our <a
+ href="dist/index.html">mirrors</a> for download.</p>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="//include/footer.include.html"?>
+</body>
+
+</html>
