I the Tutorial on (Co)datatype Definitions https://isabelle.in.tum.de/dist/Isabelle2022/doc/datatypes.pdf
in Introduction
I see the definition
datatype 'a tree_fs = Node_fs (lbl_fs:'a) (sub_fs: “'a tree_fs fset ”)
where _fs are written in subscript. Then they are used with different subscripts later on, suggesting that those subscripts are not merely a fancy design but can actually be "instantiated" in some sense. Where can I find more information about it and how can I use such subscripts?
Those subscripts can be instantiated using the predefined symbol \<^sub>, which you can insert in Isabelle/JEdit by typing \sub (literally) and choosing the down arrow icon that shows up in the dropdown list. In the specific example you refer to, you need to include a subscript for each letter f and s individually, that is, \<^sub>f\<^sub>s.
You can read more about this in The Isabelle/Isar Reference Manual, Appendix A "Predefined Isabelle symbols".