Re: [isabelle] Vector transpose



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
>
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.