Re: [isabelle] Basic use of lists
Sorry about the non-ascii symbols. I forgot to check the mail before I
I am trying to prove some lemmas about list sorting (I tried to
implement a kind of bubble sort)
But I can't. could I send the files to any one to look at?
From: nipkow at in.tum.de [mailto:nipkow at in.tum.de]
Sent: Tuesday, January 17, 2006 11:16 AM
To: Mbanefo Primrose (COM PS CE)
Cc: isabelle-users at cl.cam.ac.uk
Subject: Re: [isabelle] Basic use of lists
"sortL2 (x#xs) = (case xs of  $B"M(J [x] | y # ys $B"M(J (if (x <
y) then (y#(sortL2 (x#(ys)))) else (x#(sortL2 (y#ys))))) "
is not primrec: you are only allowed recursive calls sortL2 xs. The
tutorial describves the primrec requirement in detail. Your function
must be defined with recdef.
PS Please try to stick to ascii in your emails.
This archive was generated by a fusion of
Pipermail (Mailman edition) and