| changeset 69589 | e15f053a42d8 |
| parent 69586 | 9171d1ce5a35 |
| child 69592 | a80d8ec6c998 |
--- a/etc/options Thu Jan 03 21:36:58 2019 +0100 +++ b/etc/options Thu Jan 03 21:48:05 2019 +0100 @@ -279,6 +279,9 @@ section "Theory update" +option update_inner_syntax_cartouches : bool = false + -- "update inner syntax (types, terms, etc.) to use cartouches" + option update_mixfix_cartouches : bool = false -- "update mixfix templates to use cartouches instead of double quotes"