doc-src/Logics/logics.tex
changeset 6623 021728c71030
parent 6597 56ff27255ac8
child 7160 1135f3f8782c
equal deleted inserted replaced
6622:90583d625648 6623:021728c71030
    12 %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
    12 %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
    13 %%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
    13 %%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
    14 %%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
    14 %%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
    15 %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
    15 %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
    16 %% run    ../sedindex logics    to prepare index file
    16 %% run    ../sedindex logics    to prepare index file
    17 \title{\includegraphics[scale=0.5]{isabelle.eps} \\[4ex] Isabelle's Logics}
    17 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Isabelle's Logics}
    18 
    18 
    19 \author{{\em Lawrence C. Paulson}\\
    19 \author{{\em Lawrence C. Paulson}\\
    20         Computer Laboratory \\ University of Cambridge \\
    20         Computer Laboratory \\ University of Cambridge \\
    21         \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
    21         \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
    22         With Contributions by Tobias Nipkow and Markus Wenzel%
    22         With Contributions by Tobias Nipkow and Markus Wenzel%