Re: [isabelle] Fun vs Primrec: difference?



On 07/30/2012 09:02 AM, Christian Sternagel wrote:
a very useful command to find out what theorems are newly added as part
of some previous command (e.g., datatype, primrec, fun) is

   print_theorems

(Just type it in your *.thy file directly after the command you are
interested in).

It will give a list of all the new theorems. So you will see that when
defining a function f via primrec or via fun, both times you will get
Sorry, typo: function g





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.