src/HOL/Ord.thy
changeset 3906 5ae0e1324c56
parent 3820 46b255e140dc
child 3947 eb707467f8c5