  The system of natural deduction lay mostly dormant for some thirty  years, until the thesis of Dag Prawitz of 1965, Natural Deduction: A Proof-Theoretical Study. The order in which Prawitz presented  the normalization theorem was different from the one in Gentzen's  early thesis manuscript. Prawitz gave first a normalization theorem  and subformula property for a system of natural deduction for  classical logic. This system contains no disjunction or existence. In a second stage, he considered intuitionistic natural deduction for  the full language of predicate logic and reduced its normalization to the deletion of detour convertibilities as in the fragment of  classical logic. When Gentzen's proof of normalization came to light  in 2005, Prawitz said, in conversation with the present author, that  it is clear that Gentzen knew the result, because the remarks in the  printed thesis are so suggestive.