| changeset 4686 | 74a12e86b20b |
| parent 4390 | 57e16404c2a9 |
| child 5069 | 3ea049f7979d |
--- a/src/HOL/Induct/Com.ML Fri Mar 06 18:25:28 1998 +0100 +++ b/src/HOL/Induct/Com.ML Sat Mar 07 16:29:29 1998 +0100 @@ -54,7 +54,7 @@ goalw thy [assign_def] "s[s x/x] = s"; by (rtac ext 1); -by (simp_tac (simpset() addsplits [expand_if]) 1); +by (Simp_tac 1); qed "assign_triv"; Addsimps [assign_same, assign_different, assign_triv];