Re: [isabelle] Vector transpose



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.