Renamed letI to LetI (for consistency)
authorpaulson
Tue Jan 23 11:33:46 1996 +0100 (1996-01-23)
changeset 145019a256c8086d
parent 1449 25a7ddf9c080
child 1451 6803ecb9b198
Renamed letI to LetI (for consistency)
src/ZF/AC/WO6_WO1.ML
src/ZF/Let.ML
     1.1 --- a/src/ZF/AC/WO6_WO1.ML	Tue Jan 23 11:27:29 1996 +0100
     1.2 +++ b/src/ZF/AC/WO6_WO1.ML	Tue Jan 23 11:33:46 1996 +0100
     1.3 @@ -83,7 +83,7 @@
     1.4  (* ********************************************************************** *)
     1.5  
     1.6  goalw thy [vv1_def] "vv1(f,m,b) <= f`b";
     1.7 -by (rtac (letI RS letI) 1);
     1.8 +by (rtac (LetI RS LetI) 1);
     1.9  by (split_tac [expand_if] 1);
    1.10  by (simp_tac (ZF_ss addsimps [domain_uu_subset]) 1);
    1.11  val vv1_subset = result();
     2.1 --- a/src/ZF/Let.ML	Tue Jan 23 11:27:29 1996 +0100
     2.2 +++ b/src/ZF/Let.ML	Tue Jan 23 11:33:46 1996 +0100
     2.3 @@ -11,4 +11,4 @@
     2.4  val [prem] = goalw thy
     2.5      [Let_def] "(!!x. x=t ==> P(u(x))) ==> P(let x=t in u(x))";
     2.6  br (refl RS prem) 1;
     2.7 -qed "letI";
     2.8 +qed "LetI";