changeset 90 | 5c7a69cef18b |
parent 19 | da15d528fb19 |
child 171 | 16c4ea954511 |
--- a/ex/set.ML Fri Jun 24 15:11:39 1994 +0200 +++ b/ex/set.ML Wed Jun 29 12:04:04 1994 +0200 @@ -109,7 +109,7 @@ by (fast_tac (set_cs addEs [inj_ontoD, f_eq_gE]) 1); val bij_if_then_else = result(); -goal Lfp.thy "? X. X = Compl(g``Compl(f:: 'a=>'b``X))"; +goal Lfp.thy "? X. X = Compl(g``Compl((f:: 'a=>'b)``X))"; by (rtac exI 1); by (rtac lfp_Tarski 1); by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));