# HG changeset patch
# User paulson
# Date 822393226 -3600
# Node ID 19a256c8086d1cacda3f238ffc5d9b2c5fd963d7
# Parent  25a7ddf9c080d71683d0c16aa7817d25f4d9a748
Renamed letI to LetI (for consistency)

diff -r 25a7ddf9c080 -r 19a256c8086d src/ZF/AC/WO6_WO1.ML
--- a/src/ZF/AC/WO6_WO1.ML	Tue Jan 23 11:27:29 1996 +0100
+++ b/src/ZF/AC/WO6_WO1.ML	Tue Jan 23 11:33:46 1996 +0100
@@ -83,7 +83,7 @@
 (* ********************************************************************** *)
 
 goalw thy [vv1_def] "vv1(f,m,b) <= f`b";
-by (rtac (letI RS letI) 1);
+by (rtac (LetI RS LetI) 1);
 by (split_tac [expand_if] 1);
 by (simp_tac (ZF_ss addsimps [domain_uu_subset]) 1);
 val vv1_subset = result();
diff -r 25a7ddf9c080 -r 19a256c8086d src/ZF/Let.ML
--- 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";