author | wenzelm |
Thu, 15 Nov 2001 18:20:13 +0100 | |
changeset 12207 | 4dff931b852f |
parent 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 *) val [prem] = goalw (the_context ()) [Let_def] "(!!x. x=t ==> P(u(x))) ==> P(let x=t in u(x))"; by (rtac (refl RS prem) 1); qed "LetI";