(* Title: HOL/Proofs/Lambda/Lambda.thy Author: Tobias Nipkow Copyright 1995 TU Muenchen *) section ‹Basic definitions of Lambda-calculus› theory Lambda imports Main begin declare [[syntax_ambiguity_warning = false]] subsection ‹Lambda-terms in de Bruijn notation and substitution›