77 |
77 |
78 \maketitle |
78 \maketitle |
79 |
79 |
80 \pagenumbering{roman} \tableofcontents \clearfirst |
80 \pagenumbering{roman} \tableofcontents \clearfirst |
81 |
81 |
|
82 \part{Basic Concepts} |
82 \input{Thy/document/Introduction.tex} |
83 \input{Thy/document/Introduction.tex} |
83 \input{Thy/document/Framework.tex} |
84 \input{Thy/document/Framework.tex} |
|
85 \part{General Language Elements} |
84 \input{Thy/document/Outer_Syntax.tex} |
86 \input{Thy/document/Outer_Syntax.tex} |
85 \input{Thy/document/Document_Preparation.tex} |
87 \input{Thy/document/Document_Preparation.tex} |
86 \input{Thy/document/Spec.tex} |
88 \input{Thy/document/Spec.tex} |
87 \input{Thy/document/Proof.tex} |
89 \input{Thy/document/Proof.tex} |
88 \input{Thy/document/Inner_Syntax.tex} |
90 \input{Thy/document/Inner_Syntax.tex} |
89 \input{Thy/document/Misc.tex} |
91 \input{Thy/document/Misc.tex} |
90 \input{Thy/document/Generic.tex} |
92 \input{Thy/document/Generic.tex} |
|
93 \part{Object-Logics} |
91 \input{Thy/document/HOL_Specific.tex} |
94 \input{Thy/document/HOL_Specific.tex} |
92 \input{Thy/document/HOLCF_Specific.tex} |
95 \input{Thy/document/HOLCF_Specific.tex} |
93 \input{Thy/document/ZF_Specific.tex} |
96 \input{Thy/document/ZF_Specific.tex} |
94 |
97 |
|
98 \part{Appendix} |
95 \appendix |
99 \appendix |
96 \input{Thy/document/Quick_Reference.tex} |
100 \input{Thy/document/Quick_Reference.tex} |
97 \let\int\intorig |
101 \let\int\intorig |
98 \input{Thy/document/Symbols.tex} |
102 \input{Thy/document/Symbols.tex} |
99 \input{Thy/document/ML_Tactic.tex} |
103 \input{Thy/document/ML_Tactic.tex} |