isabelle: src/HOL/Nominal/ROOT.ML@2bda5eddadf3 (annotated)

24584 01e83ffa6c54 fixed title haftmann parents: 20809 diff changeset	1	(* Title: HOL/Nominal/ROOT.ML
19493 d8f252757460 New ROOT file for nominal datatype package. berghofe parents: diff changeset	2	Author: Stefan Berghofer and Christian Urban, TU Muenchen
d8f252757460 New ROOT file for nominal datatype package. berghofe parents: diff changeset	3
d8f252757460 New ROOT file for nominal datatype package. berghofe parents: diff changeset	4	The nominal datatype package.
d8f252757460 New ROOT file for nominal datatype package. berghofe parents: diff changeset	5	*)
d8f252757460 New ROOT file for nominal datatype package. berghofe parents: diff changeset	6
41413 64cd30d6b0b8 explicit file specifications -- avoid secondary load path; wenzelm parents: 33615 diff changeset	7	no_document use_thys ["~~/src/HOL/Library/Infinite_Set"];
33615 261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 24584 diff changeset	8	use_thys ["Nominal"];