Summary
- Moved Imperative HOL fixes from Separation_Logic_Imperative_HOL to Isabelle/HOL/Library/Imperative HOL
- Changed to work with non IntInf default int type
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) |
The file was modified | thys/Collections/Lib/Diff_Array.thy (diff) |