Nominal/Ex/SingleLet.thy
changeset 2560 82e37a4595c7
parent 2559 add799cf0817
child 2562 e8ec504dddf2
equal deleted inserted replaced
2559:add799cf0817 2560:82e37a4595c7
    33 thm single_let.size_eqvt
    33 thm single_let.size_eqvt
    34 thm single_let.supports
    34 thm single_let.supports
    35 thm single_let.fsupp
    35 thm single_let.fsupp
    36 thm single_let.supp
    36 thm single_let.supp
    37 thm single_let.fresh
    37 thm single_let.fresh
    38 
       
    39 primrec
       
    40   permute_bn_raw
       
    41 where
       
    42   "permute_bn_raw p (As_raw x y t) = As_raw (p \<bullet> x) y t"
       
    43 
    38 
    44 quotient_definition
    39 quotient_definition
    45   "permute_bn :: perm \<Rightarrow> assg \<Rightarrow> assg"
    40   "permute_bn :: perm \<Rightarrow> assg \<Rightarrow> assg"
    46 is
    41 is
    47   "permute_bn_raw"
    42   "permute_bn_raw"