src/HOL/TLA/README.html

 <LI>Theory <A HREF="TLA.html">TLA</A> axiomatizes proper temporal
   logic.
 </UL>
 
 Please consult the
-<A HREF="http://www4.in.tum.de/~merz/papers/IsaTLADesign.ps">design notes</A>
+<A HREF="http://www.pst.informatik.uni-muenchen.de/~merz/isabelle/IsaTLADesign.ps">design notes</A>
 for further information regarding the setup and use of this encoding
 of TLA.
 
 <P>
 The theories are accompanied by a small number of examples:

   in a row implement a single buffer, uses a simple refinement
   mapping.
 <LI><A HREF="Memory/index.html">Memory</A>: a verification of (the
   untimed part of) Broy and Lamport's <em>RPC-Memory</em> case study,
   more fully explained in LNCS 1169 (the 
-  <A HREF="http://www4.in.tum.de/~merz/papers/RPCMemory.html">TLA
+  <A HREF="http://www.pst.informatik.uni-muenchen.de/~merz/papers/RPCMemory.html">TLA
   solution</A> is available separately).
 </UL>
 
 <HR>