[isabelle] function package: tactic failed

Dear list,

I found an issue in some internal tactic in the function package. Here's
a minimal example:

  function iter_transform :: "'a â 'a" where
  "iter_transform rs = (if True then iter_transform rs else rs)"
  by pat_completeness auto

The problem appears to be the 'True'; if I replace it with 'undefined',
the error goes away.

(I know that the function as stated does not terminate, but that's not
the issue here.)


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