author | clasohm |
Sat, 09 Dec 1995 13:36:11 +0100 | |
changeset 1401 | 0c439768f45c |
parent 1061 | 8897213195c0 |
child 1450 | 19a256c8086d |
permissions | -rw-r--r-- |
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"; |