Theory Misc_LLang

theory Misc_LLang
imports
  "Automatic_Refinement.Misc"
begin

  (* TODO: Move *)  
  lemma map_le_empty_iff[simp]: "m m Map.empty  m=Map.empty"
    using map_le_antisym by fastforce  
    
  (* TODO: Move *)  
  lemma set_minus_minus_disj_conv: "AR={}  A - (B - R) = A - B" by auto

  (* TODO: Move *)  
  lemma ndomIff: "idom m  m i = None" by auto
  
  lemma nat_minus1_less_if_neZ[simp]: "a - Suc 0 < a  a0" by auto  

  
  ML 
    fun trace_exn msg e x = e x
      handle exn => (
        if not (Exn.is_interrupt exn) then msg () |> tracing else ();
        Exn.reraise exn
      )
  
  
  

end