doc-src/IsarImplementation/Thy/prelim.thy
changeset 21852 7f2853bd54bf
parent 20547 796ae7fa1049
child 21862 13e9febe3080
equal deleted inserted replaced
21851:030f46b8c4b5 21852:7f2853bd54bf
   117   \begin{tabular}{rcccl}
   117   \begin{tabular}{rcccl}
   118         &            & @{text "Pure"} \\
   118         &            & @{text "Pure"} \\
   119         &            & @{text "\<down>"} \\
   119         &            & @{text "\<down>"} \\
   120         &            & @{text "FOL"} \\
   120         &            & @{text "FOL"} \\
   121         & $\swarrow$ &              & $\searrow$ & \\
   121         & $\swarrow$ &              & $\searrow$ & \\
   122   $Nat$ &            &              &            & @{text "List"} \\
   122   @{text "Nat"} &    &              &            & @{text "List"} \\
   123         & $\searrow$ &              & $\swarrow$ \\
   123         & $\searrow$ &              & $\swarrow$ \\
   124         &            & @{text "Length"} \\
   124         &            & @{text "Length"} \\
   125         &            & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
   125         &            & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
   126         &            & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
   126         &            & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
   127         &            & $\vdots$~~ \\
   127         &            & $\vdots$~~ \\