// Fig. 4.7
// Assignment taclet from Example 4.4
// (the taclet given here already exists as base rule in KeY)

\schemaVariables{
  \formula phi; \program Variable #loc; \program SimpleExpression #se;
  \modalOperator { diamond, box, diamond_trc,
                   box_trc, throughout_trc } #normalMod;
}
\rules{
  assign { \find (        ==> \modality{#normalMod}
                                  {.. #loc = #se; ...}
                              \endmodality(phi) )
           \replacewith ( ==> {#loc:= #se}
                              \modality{#normalMod}
                                  {.. ...}
                              \endmodality(phi) ) };
}