author  paulson 
Tue, 23 Jan 1996 11:33:46 +0100  
changeset 1450  19a256c8086d 
parent 1061  8897213195c0 
child 1461  6bcb44e4d6e5 
permissions  rwrr 
1061  1 
(* Title: ZF/Let 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

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))"; 

13 
br (refl RS prem) 1; 

1450  14 
qed "LetI"; 