src/HOL/Data_Structures/Cmp.thy
changeset 78497 b159a5496a3e
parent 67406 23307fd33906