[isabelle-dev] Bad session structure

Lawrence Paulson lp15 at cam.ac.uk
Mon Jun 25 15:25:16 CEST 2018


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


More information about the isabelle-dev mailing list