2183   %This completes the proof showing that the weak induction principles imply 

  2183   %This completes the proof showing that the weak induction principles imply 

  2184   %the strong induction principles. 

  2184   %the strong induction principles. 

  2185 *}

  2185 *}

  2186 

  2186 

  2187 

  2187 

  2189 

  2189 

  2190 text {*

  2190 text {*

  2191   To our knowledge the earliest usage of general binders in a theorem prover

  2191   To our knowledge the earliest usage of general binders in a theorem prover

  2192   is described in \cite{NaraschewskiNipkow99} about a formalisation of the

  2192   is described in \cite{NaraschewskiNipkow99} about a formalisation of the

  2193   algorithm W. This formalisation implements binding in type-schemes using a

  2193   algorithm W. This formalisation implements binding in type-schemes using a