author | wenzelm |
Tue, 11 Mar 1997 13:05:40 +0100 | |
changeset 2781 | 0d6fcae3ae45 |
parent 1461 | 6bcb44e4d6e5 |
child 9907 | 473a6604da94 |
permissions | -rw-r--r-- |
(* 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))"; by (rtac (refl RS prem) 1); qed "LetI";