do *not* enforce scalable fonts for T1 encoding, instead rely on cm-super fonts, which also provide underscore for non-tt font;
1.1 --- a/src/Doc/IsarImplementation/document/root.tex Sun Feb 09 16:17:01 2014 +0100
1.2 +++ b/src/Doc/IsarImplementation/document/root.tex Sun Feb 09 16:31:24 2014 +0100
1.3 @@ -1,6 +1,5 @@
1.4 \documentclass[12pt,a4paper,fleqn]{report}
1.5 \usepackage[T1]{fontenc}
1.6 -\usepackage{ae}
1.7 \usepackage{latexsym,graphicx}
1.8 \usepackage[refpage]{nomencl}
1.9 \usepackage{iman,extra,isar,proof}
2.1 --- a/src/Doc/IsarRef/document/root.tex Sun Feb 09 16:17:01 2014 +0100
2.2 +++ b/src/Doc/IsarRef/document/root.tex Sun Feb 09 16:31:24 2014 +0100
2.3 @@ -1,6 +1,5 @@
2.4 \documentclass[12pt,a4paper,fleqn]{report}
2.5 \usepackage[T1]{fontenc}
2.6 -\usepackage{ae}
2.7 \usepackage{amssymb}
2.8 \usepackage{eurosym}
2.9 \usepackage[english]{babel}
3.1 --- a/src/Doc/System/document/root.tex Sun Feb 09 16:17:01 2014 +0100
3.2 +++ b/src/Doc/System/document/root.tex Sun Feb 09 16:31:24 2014 +0100
3.3 @@ -1,6 +1,5 @@
3.4 \documentclass[12pt,a4paper]{report}
3.5 \usepackage[T1]{fontenc}
3.6 -\usepackage{ae}
3.7 \usepackage{supertabular}
3.8 \usepackage{graphicx}
3.9 \usepackage{iman,extra,isar,ttbox}