src/HOL/UNITY/Lift_prog.ML
changeset 11467 1064effe37f6
parent 11170 015af2fc7026
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/UNITY/Lift_prog.ML	Mon Aug 06 15:54:29 2001 +0200
     1.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Mon Aug 06 16:43:40 2001 +0200
     1.3 @@ -309,7 +309,7 @@
     1.4  Goal "(insert_map j t f)(i := s) = \
     1.5  \     (if i=j then insert_map i s f \
     1.6  \      else if i<j then insert_map j t (f(i:=s)) \
     1.7 -\      else insert_map j t (f(i-1:=s)))";
     1.8 +\      else insert_map j t (f(i-1' := s)))";
     1.9  by (rtac ext 1);
    1.10  by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
    1.11  by (ALLGOALS arith_tac);
    1.12 @@ -341,7 +341,7 @@
    1.13  by (dtac subsetD 1);
    1.14  by (Blast_tac 1);
    1.15  by Auto_tac;
    1.16 -ren "s f uu s' f' uu'" 1;
    1.17 +by (rename_tac "s f uu s' f' uu'" 1);
    1.18  by (subgoal_tac "f'=f & uu'=uu" 1);
    1.19  by (force_tac (claset() addSDs [preserves_imp_eq], simpset()) 2);
    1.20  by Auto_tac;