[isabelle] recdef error message talks about :000



I'm trying to use recdef for the first time and I'm getting error
messages I don't understand.  Here is my problem boiled down as small as
I can make it:

consts test :: "nat list => bool"
recdef test "measure(length)"
       "test ([]) = True"
       "test ((discard#L)) = (EX L'. (L=L') /\ test L')"


*** Proof failed.
*** ALL:000 L. length :000 < Suc (length L)
***  1. ALL:000 L. length :000 < Suc (length L)
*** 1 unsolved goal(s)!
*** The error(s) above occurred for the goal statement:
*** ALL:000 L. length :000 < Suc (length L)
*** At command "recdef".


Have no idea what :000 is, or how to make this work.  Any help
appreciated.





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