author | paulson |
Tue, 18 Jun 2002 10:52:08 +0200 | |
changeset 13218 | 3732064ccbd1 |
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";