// Fig. 4.6
// Example of a taclet implementing a rule of JAVA CARD DL
// (the taclet given here already exists as base rule in KeY)

\schemaVariables {
  \formula phi;
  \program SimpleExpression #se;       \program Statement #s0, #s1;
}
\rules {
  ifElseSplit { \find (==> \<{.. if(#se) #s0 else #s1 ...}\>phi)
     "if #se true":  \replacewith (==> \<{.. #s0 ...}\>phi)
                     \add (#se = TRUE ==>);
     "if #se false": \replacewith (==> \<{.. #s1 ...}\>phi)
                     \add (#se = FALSE ==>) };
}