equal
deleted
inserted
replaced
139 (asm_simp_tac HOLCF_ss 1), |
139 (asm_simp_tac HOLCF_ss 1), |
140 (simp_tac (HOLCF_ss addsimps (prems @ stream_rews)) 1) |
140 (simp_tac (HOLCF_ss addsimps (prems @ stream_rews)) 1) |
141 ]); |
141 ]); |
142 |
142 |
143 val stream_constrdef = [ |
143 val stream_constrdef = [ |
144 prover "is_scons[UU] ~= UU" "x~=UU ==> scons[x][xs]~=UU" |
144 prover "is_scons[UU::'a stream] ~= UU" "x~=UU ==> scons[x::'a][xs]~=UU" |
145 ]; |
145 ]; |
146 |
146 |
147 fun prover defs thm = prove_goalw Stream.thy defs thm |
147 fun prover defs thm = prove_goalw Stream.thy defs thm |
148 (fn prems => |
148 (fn prems => |
149 [ |
149 [ |