*To*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Partial functions basics*From*: Roger H. <s57076 at hotmail.com>*Date*: Thu, 9 Jan 2014 19:21:58 +0200*Importance*: Normal

Hi, how can i make "f ∪ g"? definition f :: "nat ⇀ nat" where "f = [1 ↦ 0, 2 ↦ 5]" definition g :: "nat ⇀ nat" where "g = [3 ↦ 7, 4 ↦ 9]" definition f_union_g :: "nat ⇀ nat" where "f_union_g = [1 ↦ 0, 2 ↦ 5, 3 ↦ 7, 4 ↦ 9]" So how should i define f_union_g? And generally in what class.thy can i find such operators on partial functions? Thank you!

**Follow-Ups**:**Re: [isabelle] Partial functions basics***From:*John Wickerson

- Previous by Date: Re: [isabelle] Partial function simple question
- Next by Date: Re: [isabelle] Partial functions basics
- Previous by Thread: [isabelle] typedef proof method
- Next by Thread: Re: [isabelle] Partial functions basics
- Cl-isabelle-users January 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