added new website
authorhaftmann
Sat, 04 Jun 2005 10:26:08 +0200
changeset 16233 e634d33deb86
parent 16232 8a12e11d222b
child 16234 421c3522f160
added new website
Admin/website/README
Admin/website/build/img.memo.txt
Admin/website/build/localconf.at.template.mak
Admin/website/build/localconf.sun.template.mak
Admin/website/build/main.mak
Admin/website/build/mkcontents.pl
Admin/website/build/project.mak
Admin/website/build/pypager.py
Admin/website/community.html
Admin/website/dist/css/aelfwine.css
Admin/website/dist/css/isabelle_base.css
Admin/website/dist/css/isabelle_print.css
Admin/website/dist/css/isabelle_screen.css
Admin/website/dist/documentation.html
Admin/website/dist/download.html
Admin/website/dist/download_past.html
Admin/website/dist/img/favicon.ico
Admin/website/dist/img/isabelle_logo.gif
Admin/website/dist/img/screenshot_isabelle_macos.gif
Admin/website/dist/img/tutorial_cover_big.gif
Admin/website/dist/img/tutorial_cover_small.gif
Admin/website/dist/img/univ_cambridge.gif
Admin/website/dist/img/univ_tum.gif
Admin/website/dist/index.html
Admin/website/dist/installation.html
Admin/website/dist/installation_notes_cygwin.html
Admin/website/dist/installation_notes_macosx.html
Admin/website/dist/others.html
Admin/website/dtd/xhtml-lat1.ent
Admin/website/dtd/xhtml-special.ent
Admin/website/dtd/xhtml-symbol.ent
Admin/website/dtd/xhtml1-frameset.dtd
Admin/website/dtd/xhtml1-strict.dtd
Admin/website/dtd/xhtml1-transitional.dtd
Admin/website/faq.html
Admin/website/img/c_isabelle_lemmas.gif
Admin/website/img/isabelle.gif
Admin/website/img/isabelle_pg_screenshot_big.png
Admin/website/img/isabelle_pg_screenshot_small.png
Admin/website/include/documentationdist.include.html
Admin/website/include/downloadtable.include.html
Admin/website/include/footer.include.html
Admin/website/include/header.include.html
Admin/website/include/htmlheader.include.html
Admin/website/include/navigation.include.html
Admin/website/include/navigation_dist.include.html
Admin/website/index.html
Admin/website/logics.html
Admin/website/makefile
Admin/website/media/pg_preview.pdf
Admin/website/overview.html
--- /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="&#109;&#97;&#105;&#108;&#116;&#111;:&#105;&#115;&#97;&#98;&#101;&#108;&#108;&#101;-&#117;&#115;&#101;&#114;&#115;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;">&#105;&#115;&#97;&#98;&#101;&#108;&#108;&#101;-&#117;&#115;&#101;&#114;&#115;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;</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="&#109;&#97;&#105;&#108;&#116;&#111;:&#108;&#99;&#112;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;?subject=subscribe&amp;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&amp;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, &hellip;).</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 &lt;winpath&gt;</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&gt;/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&gt;/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 &ndash; 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 &amp;</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 &amp;</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   "&#160;"> <!-- no-break space = non-breaking space,
+                                  U+00A0 ISOnum -->
+<!ENTITY iexcl  "&#161;"> <!-- inverted exclamation mark, U+00A1 ISOnum -->
+<!ENTITY cent   "&#162;"> <!-- cent sign, U+00A2 ISOnum -->
+<!ENTITY pound  "&#163;"> <!-- pound sign, U+00A3 ISOnum -->
+<!ENTITY curren "&#164;"> <!-- currency sign, U+00A4 ISOnum -->
+<!ENTITY yen    "&#165;"> <!-- yen sign = yuan sign, U+00A5 ISOnum -->
+<!ENTITY brvbar "&#166;"> <!-- broken bar = broken vertical bar,
+                                  U+00A6 ISOnum -->
+<!ENTITY sect   "&#167;"> <!-- section sign, U+00A7 ISOnum -->
+<!ENTITY uml    "&#168;"> <!-- diaeresis = spacing diaeresis,
+                                  U+00A8 ISOdia -->
+<!ENTITY copy   "&#169;"> <!-- copyright sign, U+00A9 ISOnum -->
+<!ENTITY ordf   "&#170;"> <!-- feminine ordinal indicator, U+00AA ISOnum -->
+<!ENTITY laquo  "&#171;"> <!-- left-pointing double angle quotation mark
+                                  = left pointing guillemet, U+00AB ISOnum -->
+<!ENTITY not    "&#172;"> <!-- not sign = angled dash,
+                                  U+00AC ISOnum -->
+<!ENTITY shy    "&#173;"> <!-- soft hyphen = discretionary hyphen,
+                                  U+00AD ISOnum -->
+<!ENTITY reg    "&#174;"> <!-- registered sign = registered trade mark sign,
+                                  U+00AE ISOnum -->
+<!ENTITY macr   "&#175;"> <!-- macron = spacing macron = overline
+                                  = APL overbar, U+00AF ISOdia -->
+<!ENTITY deg    "&#176;"> <!-- degree sign, U+00B0 ISOnum -->
+<!ENTITY plusmn "&#177;"> <!-- plus-minus sign = plus-or-minus sign,
+                                  U+00B1 ISOnum -->
+<!ENTITY sup2   "&#178;"> <!-- superscript two = superscript digit two
+                                  = squared, U+00B2 ISOnum -->
+<!ENTITY sup3   "&#179;"> <!-- superscript three = superscript digit three
+                                  = cubed, U+00B3 ISOnum -->
+<!ENTITY acute  "&#180;"> <!-- acute accent = spacing acute,
+                                  U+00B4 ISOdia -->
+<!ENTITY micro  "&#181;"> <!-- micro sign, U+00B5 ISOnum -->
+<!ENTITY para   "&#182;"> <!-- pilcrow sign = paragraph sign,
+                                  U+00B6 ISOnum -->
+<!ENTITY middot "&#183;"> <!-- middle dot = Georgian comma
+                                  = Greek middle dot, U+00B7 ISOnum -->
+<!ENTITY cedil  "&#184;"> <!-- cedilla = spacing cedilla, U+00B8 ISOdia -->
+<!ENTITY sup1   "&#185;"> <!-- superscript one = superscript digit one,
+                                  U+00B9 ISOnum -->
+<!ENTITY ordm   "&#186;"> <!-- masculine ordinal indicator,
+                                  U+00BA ISOnum -->
+<!ENTITY raquo  "&#187;"> <!-- right-pointing double angle quotation mark
+                                  = right pointing guillemet, U+00BB ISOnum -->
+<!ENTITY frac14 "&#188;"> <!-- vulgar fraction one quarter
+                                  = fraction one quarter, U+00BC ISOnum -->
+<!ENTITY frac12 "&#189;"> <!-- vulgar fraction one half
+                                  = fraction one half, U+00BD ISOnum -->
+<!ENTITY frac34 "&#190;"> <!-- vulgar fraction three quarters
+                                  = fraction three quarters, U+00BE ISOnum -->
+<!ENTITY iquest "&#191;"> <!-- inverted question mark
+                                  = turned question mark, U+00BF ISOnum -->
+<!ENTITY Agrave "&#192;"> <!-- latin capital letter A with grave
+                                  = latin capital letter A grave,
+                                  U+00C0 ISOlat1 -->
+<!ENTITY Aacute "&#193;"> <!-- latin capital letter A with acute,
+                                  U+00C1 ISOlat1 -->
+<!ENTITY Acirc  "&#194;"> <!-- latin capital letter A with circumflex,
+                                  U+00C2 ISOlat1 -->
+<!ENTITY Atilde "&#195;"> <!-- latin capital letter A with tilde,
+                                  U+00C3 ISOlat1 -->
+<!ENTITY Auml   "&#196;"> <!-- latin capital letter A with diaeresis,
+                                  U+00C4 ISOlat1 -->
+<!ENTITY Aring  "&#197;"> <!-- latin capital letter A with ring above
+                                  = latin capital letter A ring,
+                                  U+00C5 ISOlat1 -->
+<!ENTITY AElig  "&#198;"> <!-- latin capital letter AE
+                                  = latin capital ligature AE,
+                                  U+00C6 ISOlat1 -->
+<!ENTITY Ccedil "&#199;"> <!-- latin capital letter C with cedilla,
+                                  U+00C7 ISOlat1 -->
+<!ENTITY Egrave "&#200;"> <!-- latin capital letter E with grave,
+                                  U+00C8 ISOlat1 -->
+<!ENTITY Eacute "&#201;"> <!-- latin capital letter E with acute,
+                                  U+00C9 ISOlat1 -->
+<!ENTITY Ecirc  "&#202;"> <!-- latin capital letter E with circumflex,
+                                  U+00CA ISOlat1 -->
+<!ENTITY Euml   "&#203;"> <!-- latin capital letter E with diaeresis,
+                                  U+00CB ISOlat1 -->
+<!ENTITY Igrave "&#204;"> <!-- latin capital letter I with grave,
+                                  U+00CC ISOlat1 -->
+<!ENTITY Iacute "&#205;"> <!-- latin capital letter I with acute,
+                                  U+00CD ISOlat1 -->
+<!ENTITY Icirc  "&#206;"> <!-- latin capital letter I with circumflex,
+                                  U+00CE ISOlat1 -->
+<!ENTITY Iuml   "&#207;"> <!-- latin capital letter I with diaeresis,
+                                  U+00CF ISOlat1 -->
+<!ENTITY ETH    "&#208;"> <!-- latin capital letter ETH, U+00D0 ISOlat1 -->
+<!ENTITY Ntilde "&#209;"> <!-- latin capital letter N with tilde,
+                                  U+00D1 ISOlat1 -->
+<!ENTITY Ograve "&#210;"> <!-- latin capital letter O with grave,
+                                  U+00D2 ISOlat1 -->
+<!ENTITY Oacute "&#211;"> <!-- latin capital letter O with acute,
+                                  U+00D3 ISOlat1 -->
+<!ENTITY Ocirc  "&#212;"> <!-- latin capital letter O with circumflex,
+                                  U+00D4 ISOlat1 -->
+<!ENTITY Otilde "&#213;"> <!-- latin capital letter O with tilde,
+                                  U+00D5 ISOlat1 -->
+<!ENTITY Ouml   "&#214;"> <!-- latin capital letter O with diaeresis,
+                                  U+00D6 ISOlat1 -->
+<!ENTITY times  "&#215;"> <!-- multiplication sign, U+00D7 ISOnum -->
+<!ENTITY Oslash "&#216;"> <!-- latin capital letter O with stroke
+                                  = latin capital letter O slash,
+                                  U+00D8 ISOlat1 -->
+<!ENTITY Ugrave "&#217;"> <!-- latin capital letter U with grave,
+                                  U+00D9 ISOlat1 -->
+<!ENTITY Uacute "&#218;"> <!-- latin capital letter U with acute,
+                                  U+00DA ISOlat1 -->
+<!ENTITY Ucirc  "&#219;"> <!-- latin capital letter U with circumflex,
+                                  U+00DB ISOlat1 -->
+<!ENTITY Uuml   "&#220;"> <!-- latin capital letter U with diaeresis,
+                                  U+00DC ISOlat1 -->
+<!ENTITY Yacute "&#221;"> <!-- latin capital letter Y with acute,
+                                  U+00DD ISOlat1 -->
+<!ENTITY THORN  "&#222;"> <!-- latin capital letter THORN,
+                                  U+00DE ISOlat1 -->
+<!ENTITY szlig  "&#223;"> <!-- latin small letter sharp s = ess-zed,
+                                  U+00DF ISOlat1 -->
+<!ENTITY agrave "&#224;"> <!-- latin small letter a with grave
+                                  = latin small letter a grave,
+                                  U+00E0 ISOlat1 -->
+<!ENTITY aacute "&#225;"> <!-- latin small letter a with acute,
+                                  U+00E1 ISOlat1 -->
+<!ENTITY acirc  "&#226;"> <!-- latin small letter a with circumflex,
+                                  U+00E2 ISOlat1 -->
+<!ENTITY atilde "&#227;"> <!-- latin small letter a with tilde,
+                                  U+00E3 ISOlat1 -->
+<!ENTITY auml   "&#228;"> <!-- latin small letter a with diaeresis,
+                                  U+00E4 ISOlat1 -->
+<!ENTITY aring  "&#229;"> <!-- latin small letter a with ring above
+                                  = latin small letter a ring,
+                                  U+00E5 ISOlat1 -->
+<!ENTITY aelig  "&#230;"> <!-- latin small letter ae
+                                  = latin small ligature ae, U+00E6 ISOlat1 -->
+<!ENTITY ccedil "&#231;"> <!-- latin small letter c with cedilla,
+                                  U+00E7 ISOlat1 -->
+<!ENTITY egrave "&#232;"> <!-- latin small letter e with grave,
+                                  U+00E8 ISOlat1 -->
+<!ENTITY eacute "&#233;"> <!-- latin small letter e with acute,
+                                  U+00E9 ISOlat1 -->
+<!ENTITY ecirc  "&#234;"> <!-- latin small letter e with circumflex,
+                                  U+00EA ISOlat1 -->
+<!ENTITY euml   "&#235;"> <!-- latin small letter e with diaeresis,
+                                  U+00EB ISOlat1 -->
+<!ENTITY igrave "&#236;"> <!-- latin small letter i with grave,
+                                  U+00EC ISOlat1 -->
+<!ENTITY iacute "&#237;"> <!-- latin small letter i with acute,
+                                  U+00ED ISOlat1 -->
+<!ENTITY icirc  "&#238;"> <!-- latin small letter i with circumflex,
+                                  U+00EE ISOlat1 -->
+<!ENTITY iuml   "&#239;"> <!-- latin small letter i with diaeresis,
+                                  U+00EF ISOlat1 -->
+<!ENTITY eth    "&#240;"> <!-- latin small letter eth, U+00F0 ISOlat1 -->
+<!ENTITY ntilde "&#241;"> <!-- latin small letter n with tilde,
+                                  U+00F1 ISOlat1 -->
+<!ENTITY ograve "&#242;"> <!-- latin small letter o with grave,
+                                  U+00F2 ISOlat1 -->
+<!ENTITY oacute "&#243;"> <!-- latin small letter o with acute,
+                                  U+00F3 ISOlat1 -->
+<!ENTITY ocirc  "&#244;"> <!-- latin small letter o with circumflex,
+                                  U+00F4 ISOlat1 -->
+<!ENTITY otilde "&#245;"> <!-- latin small letter o with tilde,
+                                  U+00F5 ISOlat1 -->
+<!ENTITY ouml   "&#246;"> <!-- latin small letter o with diaeresis,
+                                  U+00F6 ISOlat1 -->
+<!ENTITY divide "&#247;"> <!-- division sign, U+00F7 ISOnum -->
+<!ENTITY oslash "&#248;"> <!-- latin small letter o with stroke,
+                                  = latin small letter o slash,
+                                  U+00F8 ISOlat1 -->
+<!ENTITY ugrave "&#249;"> <!-- latin small letter u with grave,
+                                  U+00F9 ISOlat1 -->
+<!ENTITY uacute "&#250;"> <!-- latin small letter u with acute,
+                                  U+00FA ISOlat1 -->
+<!ENTITY ucirc  "&#251;"> <!-- latin small letter u with circumflex,
+                                  U+00FB ISOlat1 -->
+<!ENTITY uuml   "&#252;"> <!-- latin small letter u with diaeresis,
+                                  U+00FC ISOlat1 -->
+<!ENTITY yacute "&#253;"> <!-- latin small letter y with acute,
+                                  U+00FD ISOlat1 -->
+<!ENTITY thorn  "&#254;"> <!-- latin small letter thorn,
+                                  U+00FE ISOlat1 -->
+<!ENTITY yuml   "&#255;"> <!-- 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    "&#34;"> <!--  quotation mark, U+0022 ISOnum -->
+<!ENTITY amp     "&#38;#38;"> <!--  ampersand, U+0026 ISOnum -->
+<!ENTITY lt      "&#38;#60;"> <!--  less-than sign, U+003C ISOnum -->
+<!ENTITY gt      "&#62;"> <!--  greater-than sign, U+003E ISOnum -->
+<!ENTITY apos	 "&#39;"> <!--  apostrophe = APL quote, U+0027 ISOnum -->
+
+<!-- Latin Extended-A -->
+<!ENTITY OElig   "&#338;"> <!--  latin capital ligature OE,
+                                    U+0152 ISOlat2 -->
+<!ENTITY oelig   "&#339;"> <!--  latin small ligature oe, U+0153 ISOlat2 -->
+<!-- ligature is a misnomer, this is a separate character in some languages -->
+<!ENTITY Scaron  "&#352;"> <!--  latin capital letter S with caron,
+                                    U+0160 ISOlat2 -->
+<!ENTITY scaron  "&#353;"> <!--  latin small letter s with caron,
+                                    U+0161 ISOlat2 -->
+<!ENTITY Yuml    "&#376;"> <!--  latin capital letter Y with diaeresis,
+                                    U+0178 ISOlat2 -->
+
+<!-- Spacing Modifier Letters -->
+<!ENTITY circ    "&#710;"> <!--  modifier letter circumflex accent,
+                                    U+02C6 ISOpub -->
+<!ENTITY tilde   "&#732;"> <!--  small tilde, U+02DC ISOdia -->
+
+<!-- General Punctuation -->
+<!ENTITY ensp    "&#8194;"> <!-- en space, U+2002 ISOpub -->
+<!ENTITY emsp    "&#8195;"> <!-- em space, U+2003 ISOpub -->
+<!ENTITY thinsp  "&#8201;"> <!-- thin space, U+2009 ISOpub -->
+<!ENTITY zwnj    "&#8204;"> <!-- zero width non-joiner,
+                                    U+200C NEW RFC 2070 -->
+<!ENTITY zwj     "&#8205;"> <!-- zero width joiner, U+200D NEW RFC 2070 -->
+<!ENTITY lrm     "&#8206;"> <!-- left-to-right mark, U+200E NEW RFC 2070 -->
+<!ENTITY rlm     "&#8207;"> <!-- right-to-left mark, U+200F NEW RFC 2070 -->
+<!ENTITY ndash   "&#8211;"> <!-- en dash, U+2013 ISOpub -->
+<!ENTITY mdash   "&#8212;"> <!-- em dash, U+2014 ISOpub -->
+<!ENTITY lsquo   "&#8216;"> <!-- left single quotation mark,
+                                    U+2018 ISOnum -->
+<!ENTITY rsquo   "&#8217;"> <!-- right single quotation mark,
+                                    U+2019 ISOnum -->
+<!ENTITY sbquo   "&#8218;"> <!-- single low-9 quotation mark, U+201A NEW -->
+<!ENTITY ldquo   "&#8220;"> <!-- left double quotation mark,
+                                    U+201C ISOnum -->
+<!ENTITY rdquo   "&#8221;"> <!-- right double quotation mark,
+                                    U+201D ISOnum -->
+<!ENTITY bdquo   "&#8222;"> <!-- double low-9 quotation mark, U+201E NEW -->
+<!ENTITY dagger  "&#8224;"> <!-- dagger, U+2020 ISOpub -->
+<!ENTITY Dagger  "&#8225;"> <!-- double dagger, U+2021 ISOpub -->
+<!ENTITY permil  "&#8240;"> <!-- per mille sign, U+2030 ISOtech -->
+<!ENTITY lsaquo  "&#8249;"> <!-- single left-pointing angle quotation mark,
+                                    U+2039 ISO proposed -->
+<!-- lsaquo is proposed but not yet ISO standardized -->
+<!ENTITY rsaquo  "&#8250;"> <!-- single right-pointing angle quotation mark,
+                                    U+203A ISO proposed -->
+<!-- rsaquo is proposed but not yet ISO standardized -->
+
+<!-- Currency Symbols -->
+<!ENTITY euro   "&#8364;"> <!--  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     "&#402;"> <!-- latin small letter f with hook = function
+                                    = florin, U+0192 ISOtech -->
+
+<!-- Greek -->
+<!ENTITY Alpha    "&#913;"> <!-- greek capital letter alpha, U+0391 -->
+<!ENTITY Beta     "&#914;"> <!-- greek capital letter beta, U+0392 -->
+<!ENTITY Gamma    "&#915;"> <!-- greek capital letter gamma,
+                                    U+0393 ISOgrk3 -->
+<!ENTITY Delta    "&#916;"> <!-- greek capital letter delta,
+                                    U+0394 ISOgrk3 -->
+<!ENTITY Epsilon  "&#917;"> <!-- greek capital letter epsilon, U+0395 -->
+<!ENTITY Zeta     "&#918;"> <!-- greek capital letter zeta, U+0396 -->
+<!ENTITY Eta      "&#919;"> <!-- greek capital letter eta, U+0397 -->
+<!ENTITY Theta    "&#920;"> <!-- greek capital letter theta,
+                                    U+0398 ISOgrk3 -->
+<!ENTITY Iota     "&#921;"> <!-- greek capital letter iota, U+0399 -->
+<!ENTITY Kappa    "&#922;"> <!-- greek capital letter kappa, U+039A -->
+<!ENTITY Lambda   "&#923;"> <!-- greek capital letter lamda,
+                                    U+039B ISOgrk3 -->
+<!ENTITY Mu       "&#924;"> <!-- greek capital letter mu, U+039C -->
+<!ENTITY Nu       "&#925;"> <!-- greek capital letter nu, U+039D -->
+<!ENTITY Xi       "&#926;"> <!-- greek capital letter xi, U+039E ISOgrk3 -->
+<!ENTITY Omicron  "&#927;"> <!-- greek capital letter omicron, U+039F -->
+<!ENTITY Pi       "&#928;"> <!-- greek capital letter pi, U+03A0 ISOgrk3 -->
+<!ENTITY Rho      "&#929;"> <!-- greek capital letter rho, U+03A1 -->
+<!-- there is no Sigmaf, and no U+03A2 character either -->
+<!ENTITY Sigma    "&#931;"> <!-- greek capital letter sigma,
+                                    U+03A3 ISOgrk3 -->
+<!ENTITY Tau      "&#932;"> <!-- greek capital letter tau, U+03A4 -->
+<!ENTITY Upsilon  "&#933;"> <!-- greek capital letter upsilon,
+                                    U+03A5 ISOgrk3 -->
+<!ENTITY Phi      "&#934;"> <!-- greek capital letter phi,
+                                    U+03A6 ISOgrk3 -->
+<!ENTITY Chi      "&#935;"> <!-- greek capital letter chi, U+03A7 -->
+<!ENTITY Psi      "&#936;"> <!-- greek capital letter psi,
+                                    U+03A8 ISOgrk3 -->
+<!ENTITY Omega    "&#937;"> <!-- greek capital letter omega,
+                                    U+03A9 ISOgrk3 -->
+
+<!ENTITY alpha    "&#945;"> <!-- greek small letter alpha,
+                                    U+03B1 ISOgrk3 -->
+<!ENTITY beta     "&#946;"> <!-- greek small letter beta, U+03B2 ISOgrk3 -->
+<!ENTITY gamma    "&#947;"> <!-- greek small letter gamma,
+                                    U+03B3 ISOgrk3 -->
+<!ENTITY delta    "&#948;"> <!-- greek small letter delta,
+                                    U+03B4 ISOgrk3 -->
+<!ENTITY epsilon  "&#949;"> <!-- greek small letter epsilon,
+                                    U+03B5 ISOgrk3 -->
+<!ENTITY zeta     "&#950;"> <!-- greek small letter zeta, U+03B6 ISOgrk3 -->
+<!ENTITY eta      "&#951;"> <!-- greek small letter eta, U+03B7 ISOgrk3 -->
+<!ENTITY theta    "&#952;"> <!-- greek small letter theta,
+                                    U+03B8 ISOgrk3 -->
+<!ENTITY iota     "&#953;"> <!-- greek small letter iota, U+03B9 ISOgrk3 -->
+<!ENTITY kappa    "&#954;"> <!-- greek small letter kappa,
+                                    U+03BA ISOgrk3 -->
+<!ENTITY lambda   "&#955;"> <!-- greek small letter lamda,
+                                    U+03BB ISOgrk3 -->
+<!ENTITY mu       "&#956;"> <!-- greek small letter mu, U+03BC ISOgrk3 -->
+<!ENTITY nu       "&#957;"> <!-- greek small letter nu, U+03BD ISOgrk3 -->
+<!ENTITY xi       "&#958;"> <!-- greek small letter xi, U+03BE ISOgrk3 -->
+<!ENTITY omicron  "&#959;"> <!-- greek small letter omicron, U+03BF NEW -->
+<!ENTITY pi       "&#960;"> <!-- greek small letter pi, U+03C0 ISOgrk3 -->
+<!ENTITY rho      "&#961;"> <!-- greek small letter rho, U+03C1 ISOgrk3 -->
+<!ENTITY sigmaf   "&#962;"> <!-- greek small letter final sigma,
+                                    U+03C2 ISOgrk3 -->
+<!ENTITY sigma    "&#963;"> <!-- greek small letter sigma,
+                                    U+03C3 ISOgrk3 -->
+<!ENTITY tau      "&#964;"> <!-- greek small letter tau, U+03C4 ISOgrk3 -->
+<!ENTITY upsilon  "&#965;"> <!-- greek small letter upsilon,
+                                    U+03C5 ISOgrk3 -->
+<!ENTITY phi      "&#966;"> <!-- greek small letter phi, U+03C6 ISOgrk3 -->
+<!ENTITY chi      "&#967;"> <!-- greek small letter chi, U+03C7 ISOgrk3 -->
+<!ENTITY psi      "&#968;"> <!-- greek small letter psi, U+03C8 ISOgrk3 -->
+<!ENTITY omega    "&#969;"> <!-- greek small letter omega,
+                                    U+03C9 ISOgrk3 -->
+<!ENTITY thetasym "&#977;"> <!-- greek theta symbol,
+                                    U+03D1 NEW -->
+<!ENTITY upsih    "&#978;"> <!-- greek upsilon with hook symbol,
+                                    U+03D2 NEW -->
+<!ENTITY piv      "&#982;"> <!-- greek pi symbol, U+03D6 ISOgrk3 -->
+
+<!-- General Punctuation -->
+<!ENTITY bull     "&#8226;"> <!-- bullet = black small circle,
+                                     U+2022 ISOpub  -->
+<!-- bullet is NOT the same as bullet operator, U+2219 -->
+<!ENTITY hellip   "&#8230;"> <!-- horizontal ellipsis = three dot leader,
+                                     U+2026 ISOpub  -->
+<!ENTITY prime    "&#8242;"> <!-- prime = minutes = feet, U+2032 ISOtech -->
+<!ENTITY Prime    "&#8243;"> <!-- double prime = seconds = inches,
+                                     U+2033 ISOtech -->
+<!ENTITY oline    "&#8254;"> <!-- overline = spacing overscore,
+                                     U+203E NEW -->
+<!ENTITY frasl    "&#8260;"> <!-- fraction slash, U+2044 NEW -->
+
+<!-- Letterlike Symbols -->
+<!ENTITY weierp   "&#8472;"> <!-- script capital P = power set
+                                     = Weierstrass p, U+2118 ISOamso -->
+<!ENTITY image    "&#8465;"> <!-- black-letter capital I = imaginary part,
+                                     U+2111 ISOamso -->
+<!ENTITY real     "&#8476;"> <!-- black-letter capital R = real part symbol,
+                                     U+211C ISOamso -->
+<!ENTITY trade    "&#8482;"> <!-- trade mark sign, U+2122 ISOnum -->
+<!ENTITY alefsym  "&#8501;"> <!-- 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     "&#8592;"> <!-- leftwards arrow, U+2190 ISOnum -->
+<!ENTITY uarr     "&#8593;"> <!-- upwards arrow, U+2191 ISOnum-->
+<!ENTITY rarr     "&#8594;"> <!-- rightwards arrow, U+2192 ISOnum -->
+<!ENTITY darr     "&#8595;"> <!-- downwards arrow, U+2193 ISOnum -->
+<!ENTITY harr     "&#8596;"> <!-- left right arrow, U+2194 ISOamsa -->
+<!ENTITY crarr    "&#8629;"> <!-- downwards arrow with corner leftwards
+                                     = carriage return, U+21B5 NEW -->
+<!ENTITY lArr     "&#8656;"> <!-- 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     "&#8657;"> <!-- upwards double arrow, U+21D1 ISOamsa -->
+<!ENTITY rArr     "&#8658;"> <!-- 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     "&#8659;"> <!-- downwards double arrow, U+21D3 ISOamsa -->
+<!ENTITY hArr     "&#8660;"> <!-- left right double arrow,
+                                     U+21D4 ISOamsa -->
+
+<!-- Mathematical Operators -->
+<!ENTITY forall   "&#8704;"> <!-- for all, U+2200 ISOtech -->
+<!ENTITY part     "&#8706;"> <!-- partial differential, U+2202 ISOtech  -->
+<!ENTITY exist    "&#8707;"> <!-- there exists, U+2203 ISOtech -->
+<!ENTITY empty    "&#8709;"> <!-- empty set = null set, U+2205 ISOamso -->
+<!ENTITY nabla    "&#8711;"> <!-- nabla = backward difference,
+                                     U+2207 ISOtech -->
+<!ENTITY isin     "&#8712;"> <!-- element of, U+2208 ISOtech -->
+<!ENTITY notin    "&#8713;"> <!-- not an element of, U+2209 ISOtech -->
+<!ENTITY ni       "&#8715;"> <!-- contains as member, U+220B ISOtech -->
+<!ENTITY prod     "&#8719;"> <!-- 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      "&#8721;"> <!-- 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    "&#8722;"> <!-- minus sign, U+2212 ISOtech -->
+<!ENTITY lowast   "&#8727;"> <!-- asterisk operator, U+2217 ISOtech -->
+<!ENTITY radic    "&#8730;"> <!-- square root = radical sign,
+                                     U+221A ISOtech -->
+<!ENTITY prop     "&#8733;"> <!-- proportional to, U+221D ISOtech -->
+<!ENTITY infin    "&#8734;"> <!-- infinity, U+221E ISOtech -->
+<!ENTITY ang      "&#8736;"> <!-- angle, U+2220 ISOamso -->
+<!ENTITY and      "&#8743;"> <!-- logical and = wedge, U+2227 ISOtech -->
+<!ENTITY or       "&#8744;"> <!-- logical or = vee, U+2228 ISOtech -->
+<!ENTITY cap      "&#8745;"> <!-- intersection = cap, U+2229 ISOtech -->
+<!ENTITY cup      "&#8746;"> <!-- union = cup, U+222A ISOtech -->
+<!ENTITY int      "&#8747;"> <!-- integral, U+222B ISOtech -->
+<!ENTITY there4   "&#8756;"> <!-- therefore, U+2234 ISOtech -->
+<!ENTITY sim      "&#8764;"> <!-- 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     "&#8773;"> <!-- approximately equal to, U+2245 ISOtech -->
+<!ENTITY asymp    "&#8776;"> <!-- almost equal to = asymptotic to,
+                                     U+2248 ISOamsr -->
+<!ENTITY ne       "&#8800;"> <!-- not equal to, U+2260 ISOtech -->
+<!ENTITY equiv    "&#8801;"> <!-- identical to, U+2261 ISOtech -->
+<!ENTITY le       "&#8804;"> <!-- less-than or equal to, U+2264 ISOtech -->
+<!ENTITY ge       "&#8805;"> <!-- greater-than or equal to,
+                                     U+2265 ISOtech -->
+<!ENTITY sub      "&#8834;"> <!-- subset of, U+2282 ISOtech -->
+<!ENTITY sup      "&#8835;"> <!-- superset of, U+2283 ISOtech -->
+<!ENTITY nsub     "&#8836;"> <!-- not a subset of, U+2284 ISOamsn -->
+<!ENTITY sube     "&#8838;"> <!-- subset of or equal to, U+2286 ISOtech -->
+<!ENTITY supe     "&#8839;"> <!-- superset of or equal to,
+                                     U+2287 ISOtech -->
+<!ENTITY oplus    "&#8853;"> <!-- circled plus = direct sum,
+                                     U+2295 ISOamsb -->
+<!ENTITY otimes   "&#8855;"> <!-- circled times = vector product,
+                                     U+2297 ISOamsb -->
+<!ENTITY perp     "&#8869;"> <!-- up tack = orthogonal to = perpendicular,
+                                     U+22A5 ISOtech -->
+<!ENTITY sdot     "&#8901;"> <!-- dot operator, U+22C5 ISOamsb -->
+<!-- dot operator is NOT the same character as U+00B7 middle dot -->
+
+<!-- Miscellaneous Technical -->
+<!ENTITY lceil    "&#8968;"> <!-- left ceiling = APL upstile,
+                                     U+2308 ISOamsc  -->
+<!ENTITY rceil    "&#8969;"> <!-- right ceiling, U+2309 ISOamsc  -->
+<!ENTITY lfloor   "&#8970;"> <!-- left floor = APL downstile,
+                                     U+230A ISOamsc  -->
+<!ENTITY rfloor   "&#8971;"> <!-- right floor, U+230B ISOamsc  -->
+<!ENTITY lang     "&#9001;"> <!-- 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     "&#9002;"> <!-- 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      "&#9674;"> <!-- lozenge, U+25CA ISOpub -->
+
+<!-- Miscellaneous Symbols -->
+<!ENTITY spades   "&#9824;"> <!-- black spade suit, U+2660 ISOpub -->
+<!-- black here seems to mean filled as opposed to hollow -->
+<!ENTITY clubs    "&#9827;"> <!-- black club suit = shamrock,
+                                     U+2663 ISOpub -->
+<!ENTITY hearts   "&#9829;"> <!-- black heart suit = valentine,
+                                     U+2665 ISOpub -->
+<!ENTITY diams    "&#9830;"> <!-- 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>-&gt;</tt>, <tt>=&gt;</tt>, <tt>--&gt;</tt>, and <tt>==&gt;</tt>
+          ?</dt>
+    
+      <dd>Isabelle uses the <tt>=&gt;</tt> arrow for the function type
+          (contrary to most functional languages which use <tt>-&gt;</tt>). So
+          <tt>a =&gt; 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>--&gt;</tt> and <tt>==&gt;</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>--&gt;</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 &amp; c</tt> might not be what you intend.
+          Isabelle parses it as <tt>(a = b) &amp; c</tt>. If you want it the other
+          way around, you must set explicit parentheses as in <tt>a = (b &amp;
+          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
+          &amp; c</tt> is not what you might expect it to be: Isabelle parses it as
+          <tt>(f x = b) &amp; c</tt> (which is indeed not a proper equation). To
+          turn it into an equation you must set explicit parentheses: <tt>f x = (b
+          &amp; 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>\&lt;equiv&gt;</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
+          -&gt; Settings -&gt; 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 &amp; False ~= True | False</tt> is
+            a counterexample of <tt>A &amp; B = A | B</tt>, and <tt>A = ~B ==&gt; A
+            &amp; 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 &amp;</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 -&gt; Options -&gt; X-Symbol</tt>
+          and (if you want to save the setting for future sessions) select
+          <tt>Options -&gt; 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>\&lt;and&gt;</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>--&gt;</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>&lt;_</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 &alpha; 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 &gt; and &gt;= in addition to &lt; and
+                &lt;=</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="&#109;&#97;&#105;&#108;&#116;&#111;:&#105;&#115;&#97;&#98;&#101;&#108;&#108;&#101;-&#117;&#115;&#101;&#114;&#115;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;">&#105;&#115;&#97;&#98;&#101;&#108;&#108;&#101;-&#117;&#115;&#101;&#114;&#115;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;</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="&#109;&#97;&#105;&#108;&#116;&#111;:&#108;&#99;&#112;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;?subject=subscribe&amp;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&ouml;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>