changeset 74291 | b83fa8f3a271 |
parent 74290 | b2ad24b5a42c |
child 74318 | 3360ea6b659d |
--- a/etc/symbols Sat Sep 11 13:04:32 2021 +0200 +++ b/etc/symbols Sat Sep 11 21:16:23 2021 +0200 @@ -489,6 +489,9 @@ \<^type_syntax> argument: cartouche \<^var> argument: cartouche \<^oracle_name> argument: cartouche +\<^Const> argument: cartouche +\<^Const_> argument: cartouche +\<^Type> argument: cartouche \<^code> argument: cartouche \<^computation> argument: cartouche \<^computation_conv> argument: cartouche