Merge branch 'master' of https://git01.codeplex.com/tlaplus

general/docs/microsoft-release.txt

@@ -216,6 +216,7 @@ Version 1.5.0 - 11 May 2015
   - Improvements to the Decompose Proof command.
   - Improvements to the TLC Errors view, including ability to
     show trace in reverse order.
+  - Has some changes to the way the Toolbox handles its subwindows.
   - Fixes all known bugs in TLC's liveness checking.
   - Fixes bug in TLC that caused infinite looping if a recursively
     defined operator is used as an operator argument in its own

org.lamport.tla.toolbox.doc/html/prover/prover.html

@@ -54,8 +54,8 @@ describes how to run it from the Toolbox. 
 But before you can run TLAPS, you must install it on your computer. 
 
 Instructions for doing this, as well as an explanation of how to use
-TLAPS, is on 
-<A href="http://msr-inria.inria.fr/~doligez/tlaps/" target="_blank">the TLAPS
+TLAPS,  on 
+<A href="https://tla.msr-inria.inria.fr/tlaps/content/Home.html" target="_blank">the TLAPS
 web page</A>.&nbsp; 
 
 As described on that page, if you are using Windows, you will also have

org.lamport.tla.toolbox.doc/html/prover/runningTlaps.html

@@ -393,11 +393,12 @@ This option tells the PM what SMT solver to use. 
 
 See the  
 <a href=
-  "http://msr-inria.inria.fr/~doligez/tlaps/advanced-tutorial.html#backends"
- target="_blank">Using different backends</a>
-section of the advanced 
-<a href="http://msr-inria.inria.fr/~doligez/tlaps/"
-   target="_blank">TLAPS documentation</a>.&nbsp;
+  "https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Tactics.html#solvers"
+ target="_blank">SMT solvers</a>
+section of the 
+<a href=
+  "https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Tactics.html"
+ target="_blank">Tactics page</a>.&nbsp;
 
 (This field specifies the argument of the PM's <code>--solver</code>
 option.)