[isabelle-dev] Problem in AFP

[Florian Haftmann]

isabelle: 9a4c049f8997 tip
afp: af801987e595 tip
Running Separation_Logic_Imperative_HOL ...
*** Undefined fact: "sum_list_update_nat" (line 598 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
*** At command "from" (line 598 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
*** Undefined fact: "sum_list_update_nat" (line 580 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
*** At command "from" (line 580 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
*** Undefined fact: "sum_list_update_nat" (line 374 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
*** At command "from" (line 374 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
*** Undefined fact: "sum_list_update_nat" (line 356 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
*** At command "from" (line 356 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
Unfinished session(s): Separation_Logic_Imperative_HOL
0:02:11 elapsed time, 0:07:54 cpu time, factor 3.62

	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170803/77f6cc0c/attachment.asc>