Commit 289c8543 authored by haftmann's avatar haftmann

more connections between mset _ = mset _ and permutations

parent 713ce6d3becb
......@@ -56,11 +56,13 @@ chapter \<open>Auxiliary Definitions needed by Lem\<close>
theory "LemExtraDefs"
imports
Main
"HOL-Library.List_Permutation"
"HOL-Library.While_Combinator"
Main
"HOL-Library.While_Combinator"
"HOL-Library.List_Permutation"
begin
hide_const (open) sign
subsection \<open>General\<close>
consts failwith :: " 'a \<Rightarrow> 'b"
......
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