1 header {* Utilities for defining constants and functions *}

     1 header {* Utilities for defining constants and functions *}

     2 theory Utils imports Lambda begin

     3 theory Utils imports Lambda begin

     3 

     4 

     4 lemma beta_app:

     5 lemma beta_app:

     5   "(\<integral> x. M) \<cdot> V x \<approx> M"

     6   "(\<integral> x. M) \<cdot> V x \<approx> M"

     6   by (rule b3, rule bI)

     7   by (rule b3, rule bI)