src/Pure/net.ML
changeset 2726 e050f8bb1177
parent 2672 85d7e800d754
child 2792 6c17c5ec3d8b
equal deleted inserted replaced
2725:9453616d4b80 2726:e050f8bb1177