[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.)

Cheers
Lars




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