Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-07-05 06:38:57 -0700 (Mon, 05 Jul 1999)
Revision: 2786
Log message:
Added: Itt_logic.genAssumT : int list -> tactic
This tactical "generalizes" over a set of assumptions. The first
assumption should be for a membership judgment. For example:
...
i. H >- t in T list
...
j. H >- Q[t]
...
H >- P[t]
BY genAssumT [i; j]
1. H >- all l: T list. (Q[l] => P[l])
2. H; x: (all l: T list. (Q[l] => P[l])) >- P[t]