src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy
changeset 62337 d3996d5873dd
parent 58316 18e6cb6a5297