src/HOL/Ord.thy
changeset 1201 de2fc8cf9b6a
parent 965 24eef3860714
child 1370 7361ac9b024d
equal deleted inserted replaced
1200:d4551b1a6da7 1201:de2fc8cf9b6a