src/HOL/ex/Dense_Linear_Order_Ex.thy
changeset 23817 ee3ee9ea0d34
parent 23454 c54975167be9
child 23905 717a6cb1c659
equal deleted inserted replaced
23816:3879cb3d0ba7 23817:ee3ee9ea0d34