Manually added some newer keywords from the distribution
theory ExPS7imports "../NewParser"begin(* example 7 from Peter Sewell's bestiary *)atom_decl namenominal_datatype exp7 = EVar name| EUnit| EPair exp7 exp7| ELetRec l::"lrbs" e::"exp7" bind_set "b7s l" in l eand lrb = Assign name exp7and lrbs = Single lrb| More lrb lrbsbinder b7 :: "lrb \<Rightarrow> atom set" and b7s :: "lrbs \<Rightarrow> atom set"where "b7 (Assign x e) = {atom x}"| "b7s (Single a) = b7 a"| "b7s (More a as) = (b7 a) \<union> (b7s as)"thm exp7_lrb_lrbs.eq_iffthm exp7_lrb_lrbs.suppend