I'm studying Isabelle's encoding of (co)datatypes. I was wondering if there is a way of defining a datatype, say:
datatype 'a tree = Node 'a ('a tree fset)
and then inspecting the BNF it generates.
You can use the command print_bnfs. Moreover, of course, you can see all generated theorems by using print_theorems immediately after the definition of the datatype. Perhaps, if you need further insight, you could try exploring the ML infrastructure associated with the BNFs.
As a side note, it is possible to see a list of all available commands using the command print_commands.