Commit 15be6e7b authored by Rene Thiemann's avatar Rene Thiemann
Browse files

no unfolding, which would lead to problems in code generation (rs_set)

parent 796dc21a7173
......@@ -85,7 +85,7 @@ lemma rs_subset_list[simp]: "(rs_subset_list as bs = None) = (rs.\<alpha> as \<s
by (simp add: rs.to_sorted_list_correct)
definition rs_Union :: "('q :: linorder)rs list \<Rightarrow> 'q rs"
where [code_unfold]: "rs_Union \<equiv> foldl rs.union (rs.empty ())"
where "rs_Union \<equiv> foldl rs.union (rs.empty ())"
lemma rs_Union[simp]: "rs.\<alpha> (rs_Union qs) = \<Union> (rs.\<alpha> ` set qs)"
proof -
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment