The following rules are added:

- When expanding a goal, expand every transformation and "metas"
  attached to this goal. Usually, we have at most one transformation
  or "metas": the one which hopefully leads us to the proof. Even
  if we have several transformations applied to the same goal,
  their number is quite limited (split, inline, bisect, what else?),
  so why not open them all? And now, at last, we don't have to click
  for the second time on "split_goal_wp" to see the result of a split.

- When expanding a transformation that has a single resulting goal,
  expand that goal, too. Now, when I expand a goal and see that the
  "inline" transformation was applied, I see immediately how the
  resulting goal was handled.

- When expanding a "metas" line, expand the resulting goal, too.
  Once again, if a manipulation gives us one goal as a result,
  there is not much information in that, unless we see how that
  new goal was dealt with.

Submitted by Johannes Kanig

Currently, the builtin theory why3.HighOrd (or just HighOrd) must
be explicitly "use"-d. However, the type (HighOrd.func 'a 'b) can
be written ('a -> 'b), and the type (HighOrd.pred 'a) can be written
('a -> bool), and the application operation (HighOrd.(@)) can be
written as the usual juxtaposition. Thus, normally, you do not have
to write the qualifiers. The builtin theory why3.Bool (or just Bool)
is needed for "bool". The names "HighOrd", "func", "pred", and "(@)"
are not yet fixed and may change.

"eliminate_epsilon" tries to be smart when a lambda (or some other
comprehension form) occurs under equality or at the top of a definition.
We could go even further and replace (\ x . t) s with t[x <- s], without
lifting the lambda. I'm not sure it's worth it: we rarely write redexes
manually. They can and will appear through inlining, though.

Anyone who wants to construct epsilon-terms directly using the API
should remember that these are not Hilbert's epsilons: by writing
an epsilon term, you postulate the existence (though not necessarily
uniqueness) of the described object, and "eliminate_epsilon" will
happily convert it to an axiom expressing this existence. We only
use epsilons to write comprehensions whose soundness is guaranteed
by a background theory, e.g. lambda-calculus.

- "diverges" states that the computation may not terminate (which
  does not mean that is always diverges: just as any other effect
  annotation, this clause states a possibility of a side effect).

- "reads {}" states that the computation does not access any variable
  except those that are listed elsewhere in the specification (or the
  proper function arguments, if "reads" is in a function spec).

- "writes {}" states that the computation does not modify any mutable
  value.

- If a function definition or an abstract computation may diverge,
  but there is no "diverges" clause in the specification, a warning
  is produced. If a function definition or an abstract computation
  always terminates, but there is a "diverges" clause in the spec,
  an error is produced.

- If there is a "reads" or a "writes" clause in a function definition
  or an abstract computation, then every modified value must be listed
  in "writes" and every accessed external variable not mentioned in
  the spec must be listed in "reads". (Notice that this is a stricter
  requirement than before, when the presence of a "writes" clause
  did not require to specify "reads".) However, one does not have to
  write "reads {}" or "writes {}" if the corresponding lists are empty.