HINT_EXISTS_TAC

I added the tactic at the end of the src/1/Tactic.sml.

A few remarks:

- Michael, you mentionned something about writing a selftest but I did not see any part of 1/selftest.ml dedicated to the test of tactics
  => what would be the ideal place for this?

- I wrote a short Doc file: help/Docfiles/Tactic.HINT_EXISTS_TAC.doc

- To make it compile I had to do a slight change to the tactic's behaviour. For clarity, I recall this behaviour briefly.
  Given a goal of the form:

  ?x. P x /\ Q x /\ R x
  =============
  1. ...
  2. ...
  3. Q t
  4. ....

  Applying HINT_EXISTS_TAC yields:

  P t /\ Q t /\ R t
  =============
  1. ...
  2. ...
  3. Q t
  4. ....

  Now the change is as follows: In my original code, I was calling ASM_REWRITE_TAC in order to simplify the goal further as follows:

  P t /\ R t
  =============
  1. ...
  2. ...
  3. Q t
  4. ....
 
  However, this introduces a dependency on Rewrite.sml (which itself depends on Tactic.sml), so I removed it.

  Comments:
  * this is actually probably a good thing since the ASM_REWRITE_TAC could have induced rewrites that were not wanted by the user
  * in addition I don't think that HINT_EXISTS_TAC had anything to do in Rewrite.sml
  * this is easily circumvented at the user level by defining a tactic which calls both tactics sequentially


-- Vincent Aravantinos <vincent@encs.concordia.ca>