Tobias
On 25/06/2018 15:25, Lawrence Paulson wrote:
I still get this upon start-up. Any idea why? ebdd5508f386+ tip Larry Cannot load theory "HOL-Data_Structures.Priority_Queue" The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue" (required by "Priority_Queue_Braun.Priority_Queue_Braun") (line 7 of "/Users/lp15/isabelle/afp/devel/thys/Priority_Queue_Braun/Priority_Queue_Braun.thy") No such file: "HOL-Data_Structures.Priority_Queue" The error(s) above occurred in session "Priority_Queue_Braun" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Priority_Queue_Braun/ROOT") Cannot load theory "HOL-Data_Structures.Priority_Queue" The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue" (required by "Amortized_Complexity.Skew_Heap_Analysis" via "Skew_Heap.Skew_Heap") (line 7 of "/Users/lp15/isabelle/afp/devel/thys/Skew_Heap/Skew_Heap.thy") No such file: "HOL-Data_Structures.Priority_Queue" The error(s) above occurred in session "Amortized_Complexity" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Amortized_Complexity/ROOT") Cannot load theory "HOL-Data_Structures.Priority_Queue" The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue" (required by "Skew_Heap.Skew_Heap") (line 7 of "/Users/lp15/isabelle/afp/devel/thys/Skew_Heap/Skew_Heap.thy") No such file: "HOL-Data_Structures.Priority_Queue" The error(s) above occurred in session "Skew_Heap" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Skew_Heap/ROOT") Cannot load theory "HOL-Data_Structures.Priority_Queue" The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue" (required by "Pairing_Heap.Pairing_Heap_Tree") (line 8 of "/Users/lp15/isabelle/afp/devel/thys/Pairing_Heap/Pairing_Heap_Tree.thy") No such file: "HOL-Data_Structures.Priority_Queue" The error(s) above occurred in session "Pairing_Heap" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Pairing_Heap/ROOT") _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
