src/HOL/Tools/Function/lexicographic_order.ML
changeset 55007 0c07990363a3
parent 51958 bca32217b304
child 56231 b98813774a63
equal deleted inserted replaced
55006:ea9fc64327cb 55007:0c07990363a3