Theory Set_without_equal

(*  Title:      JinjaThreads/Basic/Set_without_equal.thy
    Author:     Andreas Lochbihler
*)

theory Set_without_equal
imports Main
begin

text ‹
  Adapt @{type "set"} code setup such that @{const "insert"}, 
  @{const "union"}, and @{term "set_of_pred"} do not generate
  sort constraint @{class equal}.
›

declare [[code drop: insert union]]

lemma insert_code [code]:
  ‹insert x (set xs) = set (x # xs)›
  by simp

lemma union_code [code]:
  ‹set xs ∪ set ys = set (xs @ ys)›
  by simp

end