author | nipkow |
Sat, 11 Mar 1995 17:46:14 +0100 | |
changeset 948 | 3647161d15d3 |
parent 947 | 812ccc91bfa0 |
child 949 | 83c588d6fee9 |
--- a/src/HOLCF/Stream.ML Sat Mar 11 11:58:21 1995 +0100 +++ b/src/HOLCF/Stream.ML Sat Mar 11 17:46:14 1995 +0100 @@ -141,7 +141,7 @@ ]); val stream_constrdef = [ - prover "is_scons[UU] ~= UU" "x~=UU ==> scons[x][xs]~=UU" + prover "is_scons[UU::'a stream] ~= UU" "x~=UU ==> scons[x::'a][xs]~=UU" ]; fun prover defs thm = prove_goalw Stream.thy defs thm