Smart constructor pattern while proving with Isabelle

While studying chapter 3 of Concrete Semantics my instructor mentionned that some of the functions there were built using the smart constructor pattern and stated that this pattern was beneficial for theorem proving.

I googled smart constructors and they seem to be used in languages like Haskell with which I'm not familiar with. Furthermore, there are not that many references of smart constructors in theorem proving.

So, what is smart constructor pattern in Isabelle and how can it help theorem proving? Maybe you can even explain it with chapter 3 of the book...