src/Pure/term_ord.ML
changeset 77752 1208ece65cca
parent 77731 48fbecc8fab1
child 77869 1156aa9db7f5