--- a/src/HOLCF/Sprod2.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Sprod2.ML Tue Mar 10 18:33:13 1998 +0100
@@ -95,7 +95,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_sprod" Sprod2.thy
-"[|is_chain(S)|] ==> range(S) <<| \
+"[|chain(S)|] ==> range(S) <<| \
\ Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
(fn prems =>
[
@@ -123,7 +123,7 @@
qed_goal "cpo_sprod" Sprod2.thy
- "is_chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
+ "chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
(fn prems =>
[
(cut_facts_tac prems 1),