removed session HOL/Subst -- now subsumed my more modern HOL/ex/Unification.thy
(* Title: HOL/Nominal/ROOT.ML Author: Stefan Berghofer and Christian Urban, TU MuenchenThe nominal datatype package.*)no_document use_thys ["~~/src/HOL/Library/Infinite_Set"];use_thys ["Nominal"];