History for Motivating Examples of Tool Interoperability

changed:
-examples are performing induction, abstraction or replacing a
-non-executable specification with an executable one. 
-
-
examples are:

 * Performing induction over time.

 * Showing that a transition system is simulated by a finite-state one.

 * Refining a clean mathematical specification with an executable one.

The need for a framework that supports such combinations has long
been recognized. For example, a combination of general higher-order
theorem proving with model checking and symbolic simulation forms
the basis of the verification methodology applied to hardware
verification at Intel.

*** Need to add many references and list explicit examples.