`HYP_TAC : string -> (thm -> thm) -> tactic`

SYNOPSIS
Applies a rule to a named hypothesis.

DESCRIPTION
Given a string s and a rule r, HYP_TAC s r applies r to the hypothesis labeled l as specified by the pattern s which can be of one of the following form:
• "l : patt", meaning apply r to hypothesis l and destruct it with patt, like REMOVE_THEN l (DESTRUCT_TAC patt o r)
• a label "l", meaning apply r to the hypothesis l, a shorthand for HYP_TAC "l : l" r
• "l : patt", meaning apply r to hypothesis l and destruct it with patt but keep hypothesis l, like USE_THEN l (DESTRUCT_TAC patt o r)

FAILURE CONDITIONS
Applied to its arguments fails if the pattern is ill-formed. When executed as a tactic, fails if it refers to non-existent hypothesis or the rule fails or do not produce a theorem of a suitable form.

EXAMPLE
Here we use the theorem MEMBER_NOT_EMPTY to obtain an element a from a non empty set s
```  # g `!s. ~(s = ) ==> (minimal n. n IN s) IN s`;;
# e (INTRO_TAC "!s; s");;
# e (HYP_TAC "s : @a. +" (REWRITE_RULE[GSYM MEMBER_NOT_EMPTY]));;
val it : goalstack = 1 subgoal (1 total)

`a IN s ==> (minimal n. n IN s) IN s`
```
next we can finish with this goal with
```  # e (MESON_TAC[MINIMAL]);;
```
Here we derive that a strictly positive number is a non negative number
```  # g `!x. &0 < x ==> &0 <= inv x`;;
# e (INTRO_TAC "!x; xgt");;
# e (HYP_TAC "xgt -> xge" (MATCH_MP REAL_LT_IMP_LE));;
val it : goalstack = 1 subgoal (1 total)

0 [`&0 < x`] (xgt)
1 [`&0 <= x`] (xge)

`&0 <= inv x`
```
then we can solve the goal with
```  # e (HYP SIMP_TAC "xge" [REAL_LE_INV]);;
```