[isabelle-dev] Duplicate theory??

[Lawrence Paulson]

Here’s a funny thing. I tried deleting Countable_Set_Type from Library.thy and got a different error (see below).

So it involved the AFP. So I updated the AFP and it works again. That’s already odd, but…

My .isabelle/etc/components is blank! No reference to afp_devel. What the hell??

Larry

> On 8 Apr 2019, at 11:42, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
> No, no changes
> Larry

Cannot load theory "HOL-Library.Cardinal_Notations"
The error(s) above occurred for theory "HOL-Library.Cardinal_Notations"
(required by "BNF_CC.Operation_Examples" via "BNF_CC.Composition" via "BNF_CC.Axiomatised_BNF_CC") (line 8 of "/Users/lp15/isabelle/afp/devel/thys/BNF_CC/Axiomatised_BNF_CC.thy")
No such file: "HOL-Library.Cardinal_Notations"
The error(s) above occurred in session "BNF_CC" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/BNF_CC/ROOT")
Cannot load theory "HOL-Library.Countable_Set_Type"
The error(s) above occurred for theory "HOL-Library.Countable_Set_Type"
(required by "Nested_Multisets_Ordinals.Unary_PCF") (line 11 of "/Users/lp15/isabelle/afp/devel/thys/Nested_Multisets_Ordinals/Unary_PCF.thy")
No such file: "HOL-Library.Countable_Set_Type"
The error(s) above occurred in session "Nested_Multisets_Ordinals" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Nested_Multisets_Ordinals/ROOT")
Cannot load theory "HOL-Library.Countable_Set_Type"
The error(s) above occurred for theory "HOL-Library.Countable_Set_Type"
(required by "CryptHOL.Misc_CryptHOL" via "Monomorphic_Monad.Monomorphic_Monad") (line 7 of "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Monomorphic_Monad.thy")
No such file: "HOL-Library.Countable_Set_Type"
The error(s) above occurred in session "CryptHOL" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/CryptHOL/ROOT")
Cannot load theory "HOL-Library.Countable_Set_Type"
The error(s) above occurred for theory "HOL-Library.Countable_Set_Type"
(required by "Monomorphic_Monad.Monomorphic_Monad") (line 7 of "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Monomorphic_Monad.thy")
No such file: "HOL-Library.Countable_Set_Type"
The error(s) above occurred in session "Monomorphic_Monad" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/ROOT")
Cannot load theory "HOL-Library.Countable_Set_Type"
The error(s) above occurred for theory "HOL-Library.Countable_Set_Type"
(required by "Sort_Encodings.Encodings" via "Sort_Encodings.G" via "Sort_Encodings.T_G_Prelim" via "Sort_Encodings.Mcalc" via "Sort_Encodings.Mono" via "Sort_Encodings.CM" via "Sort_Encodings.M" via "Sort_Encodings.TermsAndClauses" via "Sort_Encodings.Preliminaries") (line 4 of "/Users/lp15/isabelle/afp/devel/thys/Sort_Encodings/Preliminaries.thy")
No such file: "HOL-Library.Countable_Set_Type"
The error(s) above occurred in session "Sort_Encodings" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Sort_Encodings/ROOT")
Cannot load theory "HOL-Library.Countable_Set_Type"
The error(s) above occurred for theory "HOL-Library.Countable_Set_Type"
(required by "UTP-Toolkit.utp_toolkit" via "UTP-Toolkit.Countable_Set_Extra") (line 12 of "/Users/lp15/isabelle/afp/devel/thys/UTP/toolkit/Countable_Set_Extra.thy")
No such file: "HOL-Library.Countable_Set_Type"
The error(s) above occurred in session "UTP-Toolkit" (line 12 of "/Users/lp15/isabelle/afp/devel/thys/UTP/ROOT")
Cannot load theory "HOL-Library.Cardinal_Notations"
The error(s) above occurred for theory "HOL-Library.Cardinal_Notations" (line 8 of "/Users/lp15/isabelle/afp/devel/thys/BNF_Operations/ROOT")
No such file: "HOL-Library.Cardinal_Notations"
The error(s) above occurred in session "BNF_Operations" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/BNF_Operations/ROOT")