Theory BMSSP_Executable_Refinement

theory BMSSP_Executable_Refinement
  imports BMSSP_Executable_Refinement_Internal
begin

section ‹Executable Refinement›

text ‹
  This theory is the public import point for the executable refinement chain.
  The detailed refinement proof lives in
  ‹BMSSP_Executable_Refinement_Internal›.  The aliases below keep the
  outward-facing facts under the public theory name.
›

lemmas bmssp_distances_distinct_keys =
  BMSSP_Executable_Refinement_Internal.bmssp_distances_distinct_keys

lemmas bmssp_correct_executable =
  BMSSP_Executable_Refinement_Internal.bmssp_correct_executable

end