generated inducts rule by Project_Rule.projections
theory LetFunimports "../Nominal2"beginatom_decl name(* x is bound in both e1 and e2 names in p are bound only in e1 *)nominal_datatype exp = Var name| Pair exp exp| LetRec x::name p::pat e1::exp e2::exp bind x in e2, bind x "bp p" in e1and pat = PVar name| PUnit| PPair pat patbinder bp :: "pat \<Rightarrow> atom list"where "bp (PVar x) = [atom x]"| "bp (PUnit) = []"| "bp (PPair p1 p2) = bp p1 @ bp p2"end