Commit 16ec25f2 authored by haftmann's avatar haftmann

reduced dependencies on theory List_Permutation

parent de7a40fb511d
......@@ -1107,8 +1107,8 @@ lemma cone_decomp_perm:
shows "cone_decomp T qs"
using assms(1) unfolding cone_decomp_def
proof (rule direct_decomp_perm)
from assms(2) show "perm (map cone ps) (map cone qs)"
by (induct ps qs rule: perm.induct) auto
from \<open>perm ps qs\<close> show \<open>perm (map cone ps) (map cone qs)\<close>
by (simp add: perm_iff_eq_mset)
qed
lemma valid_cone_decomp_subset_Polys:
......
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