# HG changeset patch
# User huffman
# Date 1228345477 28800
# Node ID 011a6c86ab31675792b65b6e15c2a8ac56dc139e
# Parent  9d35303719b5cc72209a190afa03c7a794d625e5# Parent  da6c224a06e66833b5adfc8faa7efd658c74a4f0
merged.

diff -r 9d35303719b5 -r 011a6c86ab31 Admin/CHECKLIST
--- a/Admin/CHECKLIST	Wed Dec 03 15:00:50 2008 -0800
+++ b/Admin/CHECKLIST	Wed Dec 03 15:04:37 2008 -0800
@@ -16,18 +16,17 @@
 - check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS, ~isabelle/website;
 
 - maintain Docs:
-    Doc/Dirs
-    Distribution/doc/Contents
+    doc-src/Dirs
+    doc/Contents
 
 - maintain Logics:
     Admin/makedist
-    Distribution/build
-    Distribution/lib/Tools/makeall
-    Distribution/lib/html/index.html
-    Doc/Logics/intro.tex
-    Doc/Logics/logics.tex
+    build
+    lib/Tools/makeall
+    lib/html/index.html
+    doc-src/Logics/intro.tex
+    doc-src/Logics/logics.tex
 
 - after release: 
     commit new ~isabelle/website/include/documentationdist.include.html to website SVN
 
-$Id$
diff -r 9d35303719b5 -r 011a6c86ab31 Admin/build
--- a/Admin/build	Wed Dec 03 15:00:50 2008 -0800
+++ b/Admin/build	Wed Dec 03 15:04:37 2008 -0800
@@ -1,7 +1,5 @@
 #!/usr/bin/env bash
 #
-# $Id$
-#
 # Administrative build for Isabelle source distribution.
 
 ## global environment
@@ -14,19 +12,8 @@
 
 ## directory layout
 
-ISABELLE_DIR="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
-
-if [ -d "$ISABELLE_DIR/Distribution" ]; then
-  ISABELLE_TOOL="$ISABELLE_DIR/Distribution/bin/isabelle"
-  ISABELLE_LIB="$ISABELLE_DIR/Distribution/lib"
-  ISABELLE_SRC="$ISABELLE_DIR"
-  ISABELLE_DOC_SRC="$ISABELLE_DIR/Doc"
-else
-  ISABELLE_TOOL="$ISABELLE_DIR/bin/isabelle"
-  ISABELLE_LIB="$ISABELLE_DIR/lib"
-  ISABELLE_SRC="$ISABELLE_DIR/src"
-  ISABELLE_DOC_SRC="$ISABELLE_DIR/doc-src"
-fi
+ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
+ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
 
 
 ## diagnostics
@@ -81,7 +68,7 @@
   echo "### Building graph browser ..."
   echo "###"
 
-  cd "$ISABELLE_LIB/browser"
+  cd "$ISABELLE_HOME/lib/browser"
   make clean all || fail "Failed to build graph browser!"
 }
 
@@ -92,7 +79,7 @@
   echo "### Building documentation ..."
   echo "###"
 
-  cd "$ISABELLE_DOC_SRC"
+  cd "$ISABELLE_HOME/doc-src"
   for DOC in $(cat Dirs)
   do
     pushd "$DOC" >/dev/null
@@ -111,12 +98,12 @@
 
   type -p scalac >/dev/null || fail "Scala compiler unavailable"
 
-  pushd "$ISABELLE_SRC/Pure" >/dev/null
+  pushd "$ISABELLE_HOME/src/Pure" >/dev/null
   "$ISABELLE_TOOL" make jar || fail "Failed to build Pure.jar!"
   popd >/dev/null
 
   if [ -d "$HOME/lib/jedit/current" ]; then
-    pushd "$ISABELLE_LIB/jedit/plugin" >/dev/null
+    pushd "$ISABELLE_HOME/lib/jedit/plugin" >/dev/null
     ./mk
     [ -f ../isabelle.jar ] || fail "Failed to build jEdit plugin!"
     popd >/dev/null
diff -r 9d35303719b5 -r 011a6c86ab31 doc-src/Makefile.in
--- a/doc-src/Makefile.in	Wed Dec 03 15:00:50 2008 -0800
+++ b/doc-src/Makefile.in	Wed Dec 03 15:04:37 2008 -0800
@@ -13,7 +13,7 @@
 SEDINDEX = ../sedindex
 FIXBOOKMARKS = perl -pi ../fixbookmarks.pl
 
-DEFAULT_GARBAGE = *.aux *.log *.toc *.idx *.rai *.rao *.bbl *.ind *.ilg *.blg *.out
+DEFAULT_GARBAGE = *.aux *.log *.toc *.idx *.rai *.rao *.bbl *.ind *.ilg *.blg *.out *.lof
 DEFAULT_OUTPUT = *.dvi *.pdf *.ps
 GARBAGE =
 OUTPUT =
diff -r 9d35303719b5 -r 011a6c86ab31 src/HOL/Auth/KerberosIV_Gets.thy
diff -r 9d35303719b5 -r 011a6c86ab31 src/HOL/Auth/KerberosV.thy
diff -r 9d35303719b5 -r 011a6c86ab31 src/HOL/Auth/Kerberos_BAN_Gets.thy
diff -r 9d35303719b5 -r 011a6c86ab31 src/HOL/Auth/OtwayReesBella.thy
diff -r 9d35303719b5 -r 011a6c86ab31 src/HOL/Auth/Smartcard/EventSC.thy
diff -r 9d35303719b5 -r 011a6c86ab31 src/HOL/Auth/Smartcard/ShoupRubin.thy
diff -r 9d35303719b5 -r 011a6c86ab31 src/HOL/Auth/Smartcard/ShoupRubinBella.thy
diff -r 9d35303719b5 -r 011a6c86ab31 src/HOL/Auth/Smartcard/Smartcard.thy
diff -r 9d35303719b5 -r 011a6c86ab31 src/HOL/Library/BigO.thy
diff -r 9d35303719b5 -r 011a6c86ab31 src/HOL/Library/Ramsey.thy
diff -r 9d35303719b5 -r 011a6c86ab31 src/HOL/Library/SetsAndFunctions.thy
diff -r 9d35303719b5 -r 011a6c86ab31 src/HOL/Tools/res_reconstruct.ML