src/HOL/Quot/HQUOT.thy
changeset 8488 58e37d59c146
parent 3842 b55686a7b22c