changeset 48957 | c04001b3a753 |
parent 48956 | d54a3d39ba85 |
--- a/doc-src/IsarRef/isar-ref.tex Tue Aug 28 12:22:10 2012 +0200 +++ b/doc-src/IsarRef/isar-ref.tex Tue Aug 28 12:31:53 2012 +0200 @@ -69,9 +69,8 @@ \input{Thy/document/Inner_Syntax.tex} \input{Thy/document/Misc.tex} \input{Thy/document/Generic.tex} -\part{Object-Logics} +\part{Object-Logic} \input{Thy/document/HOL_Specific.tex} -\input{Thy/document/HOLCF_Specific.tex} \part{Appendix} \appendix