*To*: "Tao Ma" <separable at gmail.com>*Subject*: Re: [isabelle] simple lemma in ring theory*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Fri, 15 Dec 2006 16:40:02 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50f87d9a0612141801l4b3a7d32w32b6c1b2a04c4692@mail.gmail.com>*References*: <50f87d9a0612141801l4b3a7d32w32b6c1b2a04c4692@mail.gmail.com>

Dear Tao Ma,

lemma (in "domain") assumes xr: "x \<in> carrier R" and yr: "y \<in> carrier R" shows "dvd1 R x (x \<otimes> y)" using xr and yr by (unfold dvd1_def) blast Clemens

**Follow-Ups**:**Re: [isabelle] simple lemma in ring theory***From:*Tao Ma

**References**:**[isabelle] simple lemma in ring theory***From:*Tao Ma

- Previous by Date: Re: [isabelle] Isabelle-Oracle Interface
- Next by Date: Re: [isabelle] Proof General on FC6
- Previous by Thread: [isabelle] simple lemma in ring theory
- Next by Thread: Re: [isabelle] simple lemma in ring theory
- Cl-isabelle-users December 2006 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