*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] proof solution [ newbie question ]*From*: "Gregory Kulczycki" <gregwk at vt.edu>*Date*: Sun, 8 Jul 2007 12:10:43 -0400*In-reply-to*: <4690A677.7050002@in.tum.de>*References*: <15677a8b0707071311t75dcb4e3k69931327f984a1ef@mail.gmail.com> <4690A677.7050002@in.tum.de>*Sender*: gkulczycki at gmail.com

Since my original lemma said "hd xs = c and hd ys = c" I wrongly assumed that this implied that xs and ys were non-empty. The neq_Nil_conv lemma worked well for this proof. Also, the cases method answered a question I had about another proof. Thanks! Greg

**References**:**[isabelle] proof solution [ newbie question ]***From:*Gregory Kulczycki

**Re: [isabelle] proof solution [ newbie question ]***From:*Amine Chaieb

- Previous by Date: Re: [isabelle] proof solution [ newbie question ]
- Next by Date: Re: [isabelle] Starting Isabelle from within PolyML
- Previous by Thread: Re: [isabelle] proof solution [ newbie question ]
- Next by Thread: [isabelle] splicing out part of HOL function space and non-uniform definitions
- Cl-isabelle-users July 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list