| changeset 2035 | e329b36d9136 |
| parent 1459 | d12da312eff4 |
| child 3837 | d7f033c74b38 |
--- a/src/CCL/Gfp.ML Thu Sep 26 15:49:54 1996 +0200 +++ b/src/CCL/Gfp.ML Thu Sep 26 16:12:25 1996 +0200 @@ -85,7 +85,7 @@ by (rtac prem 1); by (rtac (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1); by (rtac (mono RS monoD) 1); -by (rtac (mono RS coinduct3_mono_lemma RS lfp_Tarski RS ssubst) 1); +by (stac (mono RS coinduct3_mono_lemma RS lfp_Tarski) 1); by (rtac Un_upper2 1); qed "coinduct3_lemma";