| changeset 2035 | e329b36d9136 |
| parent 1459 | d12da312eff4 |
| child 3837 | d7f033c74b38 |
--- a/src/CCL/coinduction.ML Thu Sep 26 15:49:54 1996 +0200 +++ b/src/CCL/coinduction.ML Thu Sep 26 16:12:25 1996 +0200 @@ -7,7 +7,7 @@ *) val [mono,prem] = goal Lfp.thy "[| mono(f); a : f(lfp(f)) |] ==> a : lfp(f)"; -by (rtac ((mono RS lfp_Tarski) RS ssubst) 1); +by (stac (mono RS lfp_Tarski) 1); by (rtac prem 1); qed "lfpI";