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 <[email protected]> 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") _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
