chapter Case_Studies

session Case_Studies = Instance_Lambda_Syntax +
  description {* Case studies: Church_Rosser and Standardization theorems (for both for the call-by-name and call-by-value lambda-calculus) Henkin-style semantics and HOAS 
(for the call-by-name lambda-calculus);  *}
  options [browser_info, timeout = 2400]
  theories
    All 

