1.1 --- a/src/HOL/Induct/Com.ML	Fri May 09 10:18:07 1997 +0200
     1.2 +++ b/src/HOL/Induct/Com.ML	Fri May 09 10:18:58 1997 +0200
     1.3 @@ -41,3 +41,19 @@
     1.4  (*SLOW (23s) due to proof reconstruction; needs 60s if thin_tac is omitted*)
     1.5  by (REPEAT (blast_tac (!claset addEs [exec_WHILE_case]) 1));
     1.6  qed "Function_exec";
     1.7 +
     1.8 +
     1.9 +goalw thy [assign_def] "(s[v/x])x = v";
    1.10 +by (Simp_tac 1);
    1.11 +qed "assign_same";
    1.12 +
    1.13 +goalw thy [assign_def] "!!y. y~=x ==> (s[v/x])y = s y";
    1.14 +by (Asm_simp_tac 1);
    1.15 +qed "assign_different";
    1.16 +
    1.17 +goalw thy [assign_def] "s[s x/x] = s";
    1.18 +br ext 1;
    1.19 +by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
    1.20 +qed "assign_triv";
    1.21 +
    1.22 +Addsimps [assign_same, assign_different, assign_triv];