Re: "Undeclared fact" for nullary definitions

[Chris Warburton]

I've added a 'show_theory' command which will load a given theory into
Isabelle and print out its content, including all of the automatically
defined/derived things like induction principles, etc.

Looking through this output, I can see that 'globalFOO.simps' (which we
use for things defined via 'function') appear in the 'theorems:'
section.

In this section, the only entries which appear for things defined via
'definition' (like 'global70726f642f70726f705f33332e736d74326f6e65') are
suffixed with '_def', e.g.

  global70726f642f70726f705f33332e736d74326f6e65_def:
    global70726f642f70726f705f33332e736d74326f6e65 =
    Global437573746f6d53 Global437573746f6d5a

I'll try using these instead of '.simps' for nullary definitions.