src/Pure/item_net.ML
changeset 45666 d83797ef0d2d
parent 42810 2425068fe13a
child 53941 54874871aa06
equal deleted inserted replaced
45665:129db1416717 45666:d83797ef0d2d