contains classes for implementing rules. For now, there are only
taclet rules, represented by {@link
de.uka.ilkd.key.rule.Taclet}. The package includes the
representation of applications of taclets ({@link
de.uka.ilkd.key.rule.TacletApp}) and the builders of taclets ({@link
de.uka.ilkd.key.rule.TacletBuilder}).
Last modified: Tue Nov 26 08:54:55 MET 2002
Automated use to prove sets of taclets
To actually use all this on a set of taclets you have to do the
following: Put the taclets you are interested in into a
``.key'' file, e.g.\ called ``rules.key''.