src/HOL/ex/Dense_Linear_Order_Ex.thy
changeset 29926 7dac794eec91
parent 29823 0ab754d13ccd
equal deleted inserted replaced
29878:06efd6e731c6 29926:7dac794eec91