partial_function (tailrec)

   solve_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list "

 where

   "solve_equation eq bdv = [eq, eq, eq]"

 ML {*

 @{term solve_equation}

 *}

 thm "solve_equation.simps"

 ML {*

 val thm = @{thm solve_equation.simps}

 *} ML {*

 Thm.prop_of thm

 *} ML {*

 *}