*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Code setup for Fraction_Field*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Fri, 4 Sep 2015 13:15:37 +0200*In-reply-to*: <CA+MUZ5tjP+b8Ag1V4-N-Mqnux9yT6MEK6P234GaBycB1r6360g@mail.gmail.com>*References*: <55DED10F.5030507@inf.ethz.ch> <55DEE024.3070504@informatik.tu-muenchen.de> <55E96535.7050909@inf.ethz.ch> <CA+MUZ5tjP+b8Ag1V4-N-Mqnux9yT6MEK6P234GaBycB1r6360g@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.1.0

I just slighly modified his version to move most of theorems presented in the euclidean_ring_gcd class to the euclidean_ring one.

Cheers, Manuel

**References**:**Re: [isabelle] Code setup for Fraction_Field***From:*Andreas Lochbihler

**Re: [isabelle] Code setup for Fraction_Field***From:*Jose DivasÃn

- Previous by Date: Re: [isabelle] Code setup for Fraction_Field
- Next by Date: [isabelle] New AFP entry: Converting LTL to Deterministic (Generalised) Rabin Automata
- Previous by Thread: Re: [isabelle] Code setup for Fraction_Field
- Next by Thread: Re: [isabelle] Code setup for Fraction_Field
- Cl-isabelle-users September 2015 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