nominal2: ESOP-Paper/ROOT.ML@87d1e815aa59 (annotated)

1484 dc7b049d9072 made paper to compile Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	1	quick_and_dirty := true;
2747 a5da7b6aff8f precise path to LaTeXsugar Christian Urban <urbanc@in.tum.de> parents: 2465 diff changeset	2	no_document use_thys ["~~/src/HOL/Library/LaTeXsugar",
a5da7b6aff8f precise path to LaTeXsugar Christian Urban <urbanc@in.tum.de> parents: 2465 diff changeset	3	"../Nominal/Nominal2"];
754 b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	use_thys ["Paper"];