synchronize_syntax: declare operations within the local scope of fixes/consts
(still inactive -- breaks rogue type-inference of rule_tac/where/of);
(* Title: HOL/Nominal/ROOT.ML
ID: $Id$
Author: Stefan Berghofer and Christian Urban, TU Muenchen
The nominal datatype package.
*)
no_document use_thy "Infinite_Set";
use_thy "Nominal";