Theory Native_Word_Imperative_HOL

(*  Title:      Native_Word_Imperative_HOL.thy
    Author:     Andreas Lochbihler, ETH Zurich
*)

section ‹Compatibility with Imperative/HOL›

theory Native_Word_Imperative_HOL imports
  Code_Target_Word_Base
  "HOL-Imperative_HOL.Heap_Monad"
begin

text ‹
  We add a code target that combines the translations for native words that are by default not
  supported by all PolyML versions with the adaptations for Imperative\_HOL.
›

setup ‹Code_Target.add_derived_target ("SML_word_imp", [("SML_word", I), ("SML_imp", I)])›

end