Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-19 17:12:25 -0700 (Tue, 19 Jun 2001)
Revision: 3277
Log message:
- New tacticals
onAllAssumT : (int -> tactic) -> tactic
onAllMAssumT : (int -> tactic) -> tactic
apply a tactic to all assumtions
rwAll applies a convertion to all clauses
rwcAll applies a convertion to all clauses for the given assumption
rwAllAll applies a convertion to all assumption and to the goal sequent
rwhAll,rwchAll,rwhAllAll, rwaAll,rwcaAll,rwaAllAll work by analogy
Now these tactics does not work properly (see BUGS 3.12-3.14)
- Most of the theorems on records are proved