changeset 4098 | 71e05eb27fb6 |
parent 3323 | 194ae2e0c193 |
child 4721 | c8a8482a8124 |
--- a/src/HOLCF/Discrete1.ML Mon Nov 03 12:36:48 1997 +0100 +++ b/src/HOLCF/Discrete1.ML Mon Nov 03 14:06:27 1997 +0100 @@ -22,7 +22,7 @@ goal thy "!!S::nat=>('a::term)discr. is_chain(S) ==> range(S) = {S 0}"; -by (fast_tac (!claset addEs [discr_chain0]) 1); +by (fast_tac (claset() addEs [discr_chain0]) 1); qed "discr_chain_range0"; Addsimps [discr_chain_range0];