src/HOL/Tools/watcher.ML
changeset 24681 9d4982db0742
parent 24584 01e83ffa6c54
child 25413 df27d19c35dd
equal deleted inserted replaced
24680:0d355aa59e67 24681:9d4982db0742