make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
(* Title: HOL/Nominal/ROOT.ML ID: $Id$ Author: Stefan Berghofer and Christian Urban, TU MuenchenThe nominal datatype package.*)no_document use_thy "Infinite_Set";use_thy "Nominal";