src/HOL/Lambda/document/root.bib

replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style

@Article{Matthes-Joachimski-AML,
  author =       {Felix Joachimski and Ralph Matthes},
  title =        {Short Proofs of Normalization for the simply-typed
                  $\lambda$-calculus, permutative conversions and
                  {G}{\"o}del's {T}},
  journal =      {Archive for Mathematical Logic},
  year =         2003,
  volume =       42,
  number =       1,
  pages =        {59--87}
}