rgrig/papers — comment on commit 52d68dced97602c499e53003adab3d1b2b2d331f
File: safety/code/examples/java_iter.j line 3
By rgrig:

There was a jdk0.j file with this prefix/observing.