src/Pure/ML-Systems/system_shell.ML
changeset 28691 0dafa8aa5983
parent 26504 6e87c0a60104
child 29564 f8b933a62151
equal deleted inserted replaced
28690:fc51fa5efea1 28691:0dafa8aa5983