src/HOL/Ord.thy
changeset 7249 4886664d7033
parent 7238 36e58620ffc8
child 7357 d0e16da40ea2