src/HOL/IMP/Hoare_Total_EX.thy
2016-05-01 nipkow 2016-05-01 the standard While-rule