diff options
| author | Pierre Courtieu | 2013-07-06 14:33:15 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2013-07-06 14:33:15 +0000 |
| commit | 89d0f618d8c1060d4b519c371ffde45653c9a35f (patch) | |
| tree | f5d4d7aa235fb63ee07b3d45fe2f92f97f2737c9 /isar/Example.thy | |
| parent | d723e8eb8d9db658ddf758980d603cb16682aef4 (diff) | |
Fixing #473. Now all token finishing by <symbol><dot> is considered an
end of command, except if exactly <dot><dot>
Diffstat (limited to 'isar/Example.thy')
0 files changed, 0 insertions, 0 deletions