(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. SPDX-License-Identifier: MIT *) theory Shallow_Separation_Logic imports Apartness Assertion_Language Assertion_Triple Function_Contract Locality Permissioned_Heap Precision Representability Restriction Shareable_Value Share_Map Separation_Algebra Shareable_Value Share_Map Tree_Shares Triple Weak_Triple Weakest_Precondition begin end