CookBook/Package/Ind_Intro.thy
changeset 152 8084c353d196
parent 127 74846cb0fff9
equal deleted inserted replaced
151:7e0bf13bf743 152:8084c353d196
     1 theory Ind_Intro
     1 theory Ind_Intro
     2 imports Main 
     2 imports Main 
     3 begin
     3 begin
     4 
     4 
     5 chapter {* How to Write a Definitional Package\label{chp:package} *}
     5 chapter {* How to Write a Definitional Package\label{chp:package} (TBD) *}
     6 
     6 
     7 text {*
     7 text {*
     8   \begin{flushright}
     8   \begin{flushright}
     9   {\em
     9   {\em
    10   ``My thesis is that programming is not at the bottom of the intellectual \\
    10   ``My thesis is that programming is not at the bottom of the intellectual \\