doc-src/TutorialI/Recdef/ROOT.ML

removed fixed_tr: now handled in syntax module;
replaced mixfix_typ by TypeInfer.mixfixT, which handles binders as well;
def: beta/eta contract lhs;

use "../settings";
use_thy "termination";
use_thy "Induction";
use_thy "Nested1";
use_thy "Nested2";