// Fig. 4.3
// Examples of taclets implementing propositional rules
// (the taclets given here already exist as base rules in KeY)

\schemaVariables {
  \formula phi, psi;
}
\rules {
  close    { \assumes(phi ==> phi) \closegoal };
  impRight { \find(==> phi -> psi) \replacewith(phi ==> psi) };
  cut      { \add(phi ==>); \add(==> phi) };
  mpLeft   { \assumes(phi ==>) \find(phi -> psi ==>)
                               \replacewith(psi ==>) };
}