src/HOL/Tools/Function/lexicographic_order.ML
changeset 38764 e6a18808873c
parent 36521 73ed9f18fdd3
child 39125 f45d332a90e3
equal deleted inserted replaced
38763:283f1f9969ba 38764:e6a18808873c