| changeset 70565 | d0b75c59beca |
| parent 70371 | 3f9d03571eaa |
| child 71881 | 71de0a253842 |
--- a/etc/symbols Sat Aug 17 13:39:28 2019 +0200 +++ b/etc/symbols Sat Aug 17 17:21:30 2019 +0200 @@ -429,6 +429,7 @@ \<^type_abbrev> argument: cartouche \<^type_name> argument: cartouche \<^type_syntax> argument: cartouche +\<^oracle_name> argument: cartouche \<^code> argument: cartouche \<^computation> argument: cartouche \<^computation_conv> argument: cartouche