author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 9907  473a6604da94 
permissions  rwrr 
1461  1 
(* Title: ZF/Let 
1061  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
1061  4 
Copyright 1995 University of Cambridge 
5 

6 
Let expressions  borrowed from HOL 

7 
*) 

8 

9 
open Let; 

10 

11 
val [prem] = goalw thy 

12 
[Let_def] "(!!x. x=t ==> P(u(x))) ==> P(let x=t in u(x))"; 

1461  13 
by (rtac (refl RS prem) 1); 
1450  14 
qed "LetI"; 