72  {* pushes permutations inside, raises an error if it cannot solve all permutations. *}

    72  {* pushes permutations inside, raises an error if it cannot solve all permutations. *}

    73 

    73 

    74 (* the normal version of this lemma would cause loops *)

    74 (* the normal version of this lemma would cause loops *)

    75 lemma permute_eqvt_raw[eqvt_raw]:

    75 lemma permute_eqvt_raw[eqvt_raw]:

    76   shows "p \<bullet> permute \<equiv> permute"

    76   shows "p \<bullet> permute \<equiv> permute"

    78 apply(subst permute_eqvt)

    78 apply(subst permute_eqvt)

    79 apply(simp)

    79 apply(simp)

    80 done

    80 done

    81 

    81 

    82 section {* Logical Operators *}

    82 section {* Logical Operators *}