Renamed letI to LetI (for consistency)
authorpaulson
Tue, 23 Jan 1996 11:33:46 +0100
changeset 1450 19a256c8086d
parent 1449 25a7ddf9c080
child 1451 6803ecb9b198
Renamed letI to LetI (for consistency)
src/ZF/AC/WO6_WO1.ML
src/ZF/Let.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();
--- 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";