changeset 3919 | c036caebfc75 |
parent 3457 | a8ab7c64817c |
child 4089 | 96fba19bcbe2 |
--- a/src/HOL/Induct/Com.ML Fri Oct 17 15:23:14 1997 +0200 +++ b/src/HOL/Induct/Com.ML Fri Oct 17 15:25:12 1997 +0200 @@ -53,7 +53,7 @@ goalw thy [assign_def] "s[s x/x] = s"; by (rtac ext 1); -by (simp_tac (!simpset setloop split_tac[expand_if]) 1); +by (simp_tac (!simpset addsplits [expand_if]) 1); qed "assign_triv"; Addsimps [assign_same, assign_different, assign_triv];