*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Basic help with class and instantiation*From*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Date*: Fri, 17 Aug 2012 20:47:40 +0200*Organization*: Ada @ Home*References*: <op.wiz568nrule2fv@douda-yannick> <op.wi4j9voqule2fv@douda-yannick> <502CB0B2.7040509@informatik.tu-muenchen.de> <op.wi4zq9zzule2fv@douda-yannick> <op.wi47htqmule2fv@douda-yannick>*User-agent*: Opera Mail/12.01 (Linux)

On Thu, 16 Aug 2012 16:44:43 +0200, Makarius<makarius at sketis.net> wrote:Try this one: show "(cls1_f (cls1_g (0::nat) :: int)) = (cls1_g (0::nat))" ^^^^^^And yes, this solves the unification! (Makarius is a genius :-P ) Any of this three ones do: then show "(cls1_f (cls1_g 0)) = ((cls1_g 0) :: int)" then show "((cls1_f (cls1_g 0)) :: int) = (cls1_g 0)" then show "(cls1_f ((cls1_g 0) :: int)) = (cls1_g 0)"

proof (state): step 1 goal (1 subgoal): 1. cls1_f (cls1_g (0∷nat)) = cls1_g (0∷nat) constants: […] cls1_g :: nat ⇒ int cls1_f :: int ⇒ int […]

-- “Syntactic sugar causes cancer of the semi-colons.” [1] “Structured Programming supports the law of the excluded muddle.” [1] [1]: Epigrams on Programming — Alan J. — P. Yale University

**Follow-Ups**:**Re: [isabelle] Basic help with class and instantiation***From:*Makarius

**References**:**[isabelle] Basic help with class and instantiation***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Basic help with class and instantiation***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Basic help with class and instantiation***From:*Florian Haftmann

**Re: [isabelle] Basic help with class and instantiation***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Basic help with class and instantiation***From:*Yannick Duchêne (Hibou57)

- Previous by Date: Re: [isabelle] Basic help with class and instantiation
- Next by Date: Re: [isabelle] Basic help with class and instantiation
- Previous by Thread: Re: [isabelle] Basic help with class and instantiation
- Next by Thread: Re: [isabelle] Basic help with class and instantiation
- Cl-isabelle-users August 2012 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