| changeset 4721 | c8a8482a8124 |
| parent 4423 | a129b817b58a |
| child 5068 | fb28eaa07e01 |
--- a/src/HOLCF/Discrete.ML Tue Mar 10 18:32:37 1998 +0100 +++ b/src/HOLCF/Discrete.ML Tue Mar 10 18:33:13 1998 +0100 @@ -10,7 +10,7 @@ Addsimps [undiscr_Discr]; goal thy - "!!S::nat=>('a::term)discr. is_chain(S) ==> range(%i. f(S i)) = {f(S 0)}"; + "!!S::nat=>('a::term)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"; by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1); qed "discr_chain_f_range0";