Improve help for Tower of Hanoi module overrides

specifications/tower_of_hanoi/Bits.tla

@@ -10,13 +10,34 @@
 \*
 \* Place the resulting Bits.class next to Bits.tla (and Bits.java).
 \*
+\* If TLC correctly loads Bits.class, it prints the following message at
+\* startup:
+\*
+\* @!@!@STARTMSG 2168:0 @!@!@
+\* Loading And operator override from /Hanoi.toolbox/Model_1/Bits.class with signature: 
+\* <Java Method: public static tlc2.value.IntValue Bits.And(tlc2.value.IntValue,tlc2.value.IntValue)>.
+\* @!@!@ENDMSG 2168 @!@!@
+\*
+\* If Bits.class is missing, TLC will fail to check Hanoi.tla with the
+\* following message (because of the TLA+ AND operator defined to be FALSE below):
+\*
+\* @!@!@STARTMSG 1000:1 @!@!@
+\* TLC threw an unexpected exception.
+\* This was probably caused by an error in the spec or model.
+\* See the User Output or TLC Console for clues to what happened.
+\* The exception was a java.lang.RuntimeException
+\* : Attempted to compare equality of boolean FALSE with non-boolean:
+\* 0
+\* @!@!@ENDMSG 1000 @!@!@
+\*
 \*
 \* If TLC shows an error similiar in words to:
 \*
 \* Found a Java class for module Bits, but unable to read
 \* it as a Java class object. Bits : Unsupported major.minor version 52.0
 \*
 \* compile Bits.java with a Java version identical to the Toolbox's VM.
+\* 
 \*
 LOCAL And(x,y) == FALSE
 
@@ -27,5 +48,5 @@ x & y == And(x, y) \* Infix variant of And(x,y)
 
 =============================================================================
 \* Modification History
-\* Last modified Thu Jun 30 23:25:12 CEST 2016 by markus
+\* Last modified Thu April 25 10:56:12 CEST 2018 by markus
 \* Created Mon May 16 15:09:18 CEST 2016 by markus