[isabelle-dev] Bad session structure

[Tobias Nipkow]

This is because of a name change in the distribution. The AFP has been updated 
some 10 minutes later but your test run still saw the old version. It should 
work now.

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180625/e797157a/attachment.bin>