Nominal/Nominal2_Base.thy
changeset 3152 da59c94bed7e
parent 3147 d24e70483051
child 3167 c25386402f6a
equal deleted inserted replaced
3151:16e6140225af 3152:da59c94bed7e
   627 
   627 
   628 quotient_definition
   628 quotient_definition
   629   "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   629   "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   630 is
   630 is
   631   "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
   631   "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
       
   632   by (simp add: set_eqvt[symmetric])
   632 
   633 
   633 instance 
   634 instance 
   634 proof
   635 proof
   635   fix x :: "'a fset" and p q :: "perm"
   636   fix x :: "'a fset" and p q :: "perm"
   636   show "0 \<bullet> x = x" by (descending) (simp)
   637   show "0 \<bullet> x = x" by (descending) (simp)