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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
