(* Title: ZF/Let ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge Let expressions -- borrowed from HOL *) open Let; val [prem] = goalw thy [Let_def] "(!!x. x=t ==> P(u(x))) ==> P(let x=t in u(x))"; br (refl RS prem) 1; qed "LetI";