The hypothesis facility assigns a special role to expressions of the
form `?x || ?y , ?z`, which are intended to denote `?y` if
`?x` denotes `true` and `?z` otherwise. In other words,
these are expressions defined by cases.

Expressions with infix `||` must have second argument a pair, or
they will be rejected by the declaration checking functions of the
prover (the user can create terms which violate this restriction, but
they cannot appear in theorems). `||` now has some built-in
execution behaviour: if `?x` evaluates to `true` or `
false` under a tactic interpreter, the case expression will evaluate
to the appropriate one of `?y` and `?z`. The subterm `?x`
is handled by the tactic interpreter before the subterms `?y` or
`?z`; conditional expressions can exhibit non-strict execution
behavior.

If the subterm matching `?x` is actually an equation `?a =
?b`, then this equation is usable as a theorem in the context
matching `?y`. Moreover, any case expression with the same
equation in the position matching `?x` appearing in either the
context matching `?y` or the context matching `?z` can be
reduced to one of the alternatives (the left alternative inside `
?y` and the right alternative inside `?z`).

A theorem of the form `0 |-| n`, where *n* is a positive integer,
represents the *n*th hypothesis from the top level of the current
term, in the form of an equation applicable in the context matched by
`?y` in our generic case expression. A theorem of the form `1
|-| n` represents the same hypothesis in a form usable to decide case
expressions with the same hypothesis. A theorem of the form `(2
|-| n)@parameter` has the same effect as `1 |-| n`, except that
when applied in reverse (the only way it is likely to be applied) the
parameter is used as the value in the newly introduced case. Mark2
controls what hypotheses are available in what contexts. The `
lookhyp` and `lookhyps` commands can be used to look at
hypotheses. Theorems with infix `|-|` appearing in theorems will
have their numerals adjusted appropriately on application so that the
theorems reference the intended hypotheses.

Fri Sep 5 16:28:58 MDT 1997