src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy
changeset 60299 5ae2a2e74c93
parent 58316 18e6cb6a5297