Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Moved Imperative HOL fixes from Separation_Logic_Imperative_HOL to Isabelle/HOL/Library/Imperative HOL
  2. Changed to work with non IntInf default int type
Changeset 7963:7b03a206104b by lammich _lammich@in.tum.de_:
Moved Imperative HOL fixes from Separation_Logic_Imperative_HOL to Isabelle/HOL/Library/Imperative HOL
The file was modified thys/Refine_Imperative_HOL/benchmarks/Dijkstra/isabelle/dijkstra_export.sml (diff)
The file was modified thys/Refine_Imperative_HOL/benchmarks/Heapmap/isabelle/heapmap_export.sml (diff)
The file was modified thys/Refine_Imperative_HOL/benchmarks/NestedDFS/isabelle/NDFS_Benchmark_export.sml (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Examples/Array_Blit.thy (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Tools/Imperative_HOL_Add.thy (diff)
Changeset 7962:cb79d8b48111 by lammich _lammich@in.tum.de_:
Changed to work with non IntInf default int type
The file was modified thys/Collections/Lib/Diff_Array.thy (diff)