diff -r 9ef3db99f24a -r e1aac05fe537 Admin/page/index.html --- a/Admin/page/index.html Mon Nov 02 21:36:48 1998 +0100 +++ b/Admin/page/index.html Mon Nov 02 21:57:49 1998 +0100 @@ -1,7 +1,7 @@ -<-- $Id$ --> + Isabelle