src/ZF/Let.ML
changeset 1450 19a256c8086d
parent 1061 8897213195c0
child 1461 6bcb44e4d6e5
--- a/src/ZF/Let.ML	Tue Jan 23 11:27:29 1996 +0100
+++ b/src/ZF/Let.ML	Tue Jan 23 11:33:46 1996 +0100
@@ -11,4 +11,4 @@
 val [prem] = goalw thy
     [Let_def] "(!!x. x=t ==> P(u(x))) ==> P(let x=t in u(x))";
 br (refl RS prem) 1;
-qed "letI";
+qed "LetI";