src/HOL/Ord.ML
changeset 6315 ed71bedf6976
parent 6301 08245f5a436d
child 6433 228237ec56e5
equal deleted inserted replaced
6314:47c801a77f32 6315:ed71bedf6976