diff options
| author | Makarius Wenzel | 2000-06-03 22:17:20 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2000-06-03 22:17:20 +0000 |
| commit | 23d43d7e9335003b2f362b6ac223b419f6714382 (patch) | |
| tree | 27b1f83b41897877571a6ef40c76933a1a9cafe4 /html/functions.php3 | |
| parent | 70f99119285a02089b32c54c758e2d8a59680a71 (diff) | |
improved proof-segment-up-to-cmdstart: handle overlap of command
prefix and comment/string (e.g. { vs {* in Isar);
Diffstat (limited to 'html/functions.php3')
0 files changed, 0 insertions, 0 deletions