| changeset 4477 | b3e5857d8d99 |
| parent 4089 | 96fba19bcbe2 |
| child 4535 | f24cebc299e4 |
--- a/src/HOL/Sum.ML Tue Dec 23 11:56:09 1997 +0100 +++ b/src/HOL/Sum.ML Wed Dec 24 10:02:30 1997 +0100 @@ -149,7 +149,7 @@ goal Sum.thy "R(sum_case f g s) = \ \ ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))"; by (res_inst_tac [("s","s")] sumE 1); -by (Auto_tac()); +by Auto_tac; qed "expand_sum_case"; (*Prevents simplification of f and g: much faster*)