src/HOL/Tools/Function/lexicographic_order.ML
changeset 54887 83bf0ae03c50
parent 51958 bca32217b304
child 56231 b98813774a63
equal deleted inserted replaced
54886:3774542df61b 54887:83bf0ae03c50