*To*: mahmoud abdelazim <m.abdelazim at icloud.com>*Subject*: Re: [isabelle] Ambiguous input*From*: Lars Hupel <hupel at in.tum.de>*Date*: Thu, 27 Nov 2014 15:45:57 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <9F1634CC-C88F-41BE-8A32-813B46921EFA@icloud.com>*References*: <9F1634CC-C88F-41BE-8A32-813B46921EFA@icloud.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.2.0

> in Test.thy file i have made an abbreviation subset_b > but in output it gave me in output an Ambiguous input but i don’t know why ? and where is the problem ? The problem already occurs earlier, in your function definition: > Variable "subst" occurs on right hand side only: > ⋀x a a1 a2 subst. substb x a (Less a1 a2) = Less (subst x a a1) (subst x a a2) It seems to me that you defined "subst" somewhere else, but didn't include it in the theory file you attached. After fixing this, the ambiguity error goes away. You might still want to define some other syntax, or at least give a fixity annotation, because "[a/b]" could also denote the list containing the value "a/b".

**Follow-Ups**:**Re: [isabelle] Ambiguous input***From:*René Thiemann

**References**:**[isabelle] Ambiguous input***From:*mahmoud abdelazim

- Previous by Date: [isabelle] Ambiguous input
- Next by Date: Re: [isabelle] Ambiguous input
- Previous by Thread: [isabelle] Ambiguous input
- Next by Thread: Re: [isabelle] Ambiguous input
- Cl-isabelle-users November 2014 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