diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2000-12-28 17:49:32 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2000-12-28 17:49:32 +0000 |
| commit | acc622e1fcca27be821f9acf03fdfb8adc42dcd3 (patch) | |
| tree | 9c83e4d29aa9c3d4e075cfc9369850bae1a234ef /html/links.html | |
| parent | 565299507f49aaa8a0c70242b34b4d41d2c5b160 (diff) | |
include x-symbol-isabelle-font-lock-keywords in shell/goals/response buffers;
more robust \<^sync>;
Diffstat (limited to 'html/links.html')
0 files changed, 0 insertions, 0 deletions