[isabelle] Exception THM 0 raised (line 86 of tactic.ML)



Hi all,

in playing around with 'fun', I ran into the following exception:

exception THM 0 raised (line 86 of "tactic.ML"):
  rule_by_tactic

The code that caused this was:
fun foo where
 "foo True  False False False = True"
|"foo False True  False False = True"
|"foo False False True  False = True"
|"foo False False False True  = True"
|"foo  _    _     _     _     = False"

The same happens if I just write:
function (sequential) foo where
 "foo True  False False False = True"
|"foo False True  False False = True"
|"foo False False True  False = True"
|"foo False False False True  = True"
|"foo  _    _     _     _     = False" sorry

I hope this is not intended behavior?

Best,

Sebastiaan




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