equal
  deleted
  inserted
  replaced
  
    
    
   135 during the Ming Dynasty with a rich <A  | 
   135 during the Ming Dynasty with a rich <A  | 
   136 HREF="http://www.cityofnanjing.com">cultural heritage</A>.    | 
   136 HREF="http://www.cityofnanjing.com">cultural heritage</A>.    | 
   137 The proceedings will be published as usual in the LNCS  | 
   137 The proceedings will be published as usual in the LNCS  | 
   138 Series. There will be an  | 
   138 Series. There will be an  | 
   139 <A HREF="http://www21.in.tum.de/~nipkow/isa-tut-itp15.html">Isabelle tutorial</A> before the  | 
   139 <A HREF="http://www21.in.tum.de/~nipkow/isa-tut-itp15.html">Isabelle tutorial</A> before the  | 
   140 conference (21 - 23 August), and<BR><BR>  | 
   140 conference (21 - 23 August), and  | 
   141 a <A HREF="http://www.strub.nu/coq-itp-15">Coq tutorial</A> after the conference  | 
   141 a <A HREF="http://www.strub.nu/coq-itp-15">Coq tutorial</A> after the conference  | 
   142 (27 - 29 August).  | 
   142 (27 - 29 August).  | 
   143   | 
   143   | 
   144 <p>  | 
   144 <p>  | 
   145 <IMG SRC="pics/new.gif" ALT="" style="" align="left"><A HREF="prog.pdf">Preliminary programme</A><BR><BR>  | 
   145 <IMG SRC="pics/new.gif" ALT="" style="" align="left"><A HREF="prog.pdf">Preliminary programme</A><BR><BR>  |