*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Vector transpose*From*: Omar Jasim <oajasim1 at sheffield.ac.uk>*Date*: Tue, 27 Feb 2018 12:20:17 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>*In-reply-to*: <68f6ad9b-4697-c321-b24c-61b79471c1a2@sketis.net>*References*: <CAAi=ges=qAOTHHMFO3Tz2viX6eBKY_zKPKVQ6RWpGLwE+0AS1g@mail.gmail.com> <FDFF8848-06A0-4300-AF7B-ADBB9F30A489@exchange.uibk.ac.at> <CAAi=gevK1B1sGOyoRD4b1jSdCgkytQLV_=z2ckFHhpK+81Hg2g@mail.gmail.com> <68f6ad9b-4697-c321-b24c-61b79471c1a2@sketis.net>

My theory name is different but I think that there are two different theories which have the same name "Matrix.thy". The first "HOL/Matrix_LP/Matrix.thy" and the second " Jordan_Normal_Form/Matrix.thy". Omar On 27 February 2018 at 12:11, Makarius <makarius at sketis.net> wrote: > On 27/02/18 12:44, Omar Jasim wrote: > > However, the called theory from AFP "imports > Perron_Frobenius.HMA_Connect" is loaded > > with all associated theories but I have the following error message: > > > > exception THEORY raised (line 230 of "context.ML"): > > Duplicate theory name > > {..., Complex, MacLaurin, Complex_Main, Lattice_Algebras, Draft.Matrix} > > {..., Factorial_Ring, Missing_Ring, Module, Ring_Hom, > > Jordan_Normal_Form.Matrix} > > The theory name Matrix is already used in session Jordan_Normal_Form, so > you need to rename your own theory -- it appears as Draft.Matrix above. > (Draft is the implicit session name for the PIDE editor session). > > > Makarius > >

**Follow-Ups**:**Re: [isabelle] Vector transpose***From:*Makarius

**[isabelle] counterexamples to Euler's conjecture with Isabelle***From:*Dr A. Koutsoukou-Argyraki

**References**:**[isabelle] Vector transpose***From:*Omar Jasim

**Re: [isabelle] Vector transpose***From:*Thiemann, Rene

**Re: [isabelle] Vector transpose***From:*Omar Jasim

**Re: [isabelle] Vector transpose***From:*Makarius

- Previous by Date: Re: [isabelle] Vector transpose
- Next by Date: Re: [isabelle] 1/0 = 0?
- Previous by Thread: Re: [isabelle] Vector transpose
- Next by Thread: Re: [isabelle] Vector transpose
- Cl-isabelle-users February 2018 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