src/HOLCF/ax_ops/thy_syntax.ML
changeset 4121 390e10ddadf2
parent 3622 85898be702b2
equal deleted inserted replaced
4120:57c1e7d70960 4121:390e10ddadf2