doc-src/Ref/simp.tex
changeset 286 e7efbf03562b
parent 104 d8205bb279a7
child 323 361a71713176
equal deleted inserted replaced
285:fd4a6585e5bf 286:e7efbf03562b
    20 
    20 
    21 For many of Isabelle's logics ({\tt FOL}, {\tt ZF}, {\tt LCF} and {\tt HOL})
    21 For many of Isabelle's logics ({\tt FOL}, {\tt ZF}, {\tt LCF} and {\tt HOL})
    22 the simplifier has been set up already. Hence we start by describing the
    22 the simplifier has been set up already. Hence we start by describing the
    23 functions provided by the simplifier --- those functions exported by
    23 functions provided by the simplifier --- those functions exported by
    24 \ttindex{SimpFun} through its result signature \ttindex{SIMP} shown in
    24 \ttindex{SimpFun} through its result signature \ttindex{SIMP} shown in
    25 Figure~\ref{SIMP}.  
    25 Fig.\ts\ref{SIMP}.  
    26 
    26 
    27 
    27 
    28 \section{Simplification sets}
    28 \section{Simplification sets}
    29 \index{simplification sets}
    29 \index{simplification sets}
    30 The simplification tactics are controlled by {\bf simpsets}, which consist of
    30 The simplification tactics are controlled by {\bf simpsets}, which consist of