*To*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Subject*: Re: [isabelle] Question about functions with equal names defined in different theories*From*: Makarius <makarius at sketis.net>*Date*: Wed, 22 Sep 2010 17:11:05 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Peter Lammich <peter.lammich at uni-muenster.de>*In-reply-to*: <4C99E196.5060001@kit.edu>*References*: <4C99CB28.8090100@uni-muenster.de> <4C99E196.5060001@kit.edu>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Wed, 22 Sep 2010, Andreas Lochbihler wrote:

theory Foo imports Main begin definition foldl :: "nat" where "foldl = 0" notation List.foldl ("foldl") term "foldl" -- "List.foldl" no_notation List.fold ("foldl") term "foldl" -- "Foo.foldl" end

setup {* Sign.const_alias @{binding fold} @{const_name List.foldr} *} hide_const List.foldr term fold term foldr -- "free variable"

Makarius

**References**:**[isabelle] Question about functions with equal names defined in different theories***From:*Peter Lammich

**Re: [isabelle] Question about functions with equal names defined in different theories***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Question about functions with equal names defined in different theories
- Next by Date: Re: [isabelle] FuncSet without extensional? (Joachim Breitner)
- Previous by Thread: Re: [isabelle] Question about functions with equal names defined in different theories
- Next by Thread: [isabelle] Instantiating a quantifier in a tactic
- Cl-isabelle-users September 2010 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