author  lcp 
Fri, 14 Apr 1995 12:03:15 +0200  
changeset 1061  8897213195c0 
child 1450  19a256c8086d 
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; 

14 
qed "letI"; 