1115   If the simplifier cannot make any progress, then it leaves the goal unchanged,

  1115   If the simplifier cannot make any progress, then it leaves the goal unchanged,

  1116   i.e., does not raise any error message. That means if you use it to unfold a 

  1116   i.e., does not raise any error message. That means if you use it to unfold a 

  1117   definition for a constant and this constant is not present in the goal state, 

  1117   definition for a constant and this constant is not present in the goal state, 

  1118   you can still safely apply the simplifier.

  1118   you can still safely apply the simplifier.

  1119 

  1119 

  1120   When using the simplifier, the crucial information you have to provide is

  1123   When using the simplifier, the crucial information you have to provide is

  1121   the simpset. If this information is not handled with care, then the

  1124   the simpset. If this information is not handled with care, then the

  1122   simplifier can easily run into a loop. Therefore a good rule of thumb is to

  1125   simplifier can easily run into a loop. Therefore a good rule of thumb is to

  1123   use simpsets that are as minimal as possible. It might be surprising that a

  1126   use simpsets that are as minimal as possible. It might be surprising that a

  1124   simpset is more complex than just a simple collection of theorems used as

  1127   simpset is more complex than just a simple collection of theorems used as