doc-src/Ref/simp.tex
changeset 9695 ec7d7f877712
parent 1100 74921c7613e7
child 11181 d04f57b91166
equal deleted inserted replaced
9694:13f3aaf12be2 9695:ec7d7f877712
   487 The wildcard pattern {\tt_} matches the coercion function.
   487 The wildcard pattern {\tt_} matches the coercion function.
   488 \end{ttdescription}
   488 \end{ttdescription}
   489 
   489 
   490 
   490 
   491 \section{A sample instantiation}
   491 \section{A sample instantiation}
   492 Here is the instantiation of {\tt SIMP_DATA} for {\FOL}.  The code for {\tt
   492 Here is the instantiation of {\tt SIMP_DATA} for FOL.  The code for {\tt
   493 mk_rew_rules} is not shown; see the file {\tt FOL/simpdata.ML}.
   493   mk_rew_rules} is not shown; see the file {\tt FOL/simpdata.ML}.
   494 \begin{ttbox}
   494 \begin{ttbox}
   495 structure FOL_SimpData : SIMP_DATA =
   495 structure FOL_SimpData : SIMP_DATA =
   496   struct
   496   struct
   497   val refl_thms      = [ \(\Var{x}=\Var{x}\), \(\Var{P}\bimp\Var{P}\) ]
   497   val refl_thms      = [ \(\Var{x}=\Var{x}\), \(\Var{P}\bimp\Var{P}\) ]
   498   val trans_thms     = [ \(\List{\Var{x}=\Var{y};\Var{y}=\Var{z}}\Imp\Var{x}=\Var{z}\),
   498   val trans_thms     = [ \(\List{\Var{x}=\Var{y};\Var{y}=\Var{z}}\Imp\Var{x}=\Var{z}\),