equal
deleted
inserted
replaced
398 |
398 |
399 Goal "monotone f A r"; |
399 Goal "monotone f A r"; |
400 by (simp_tac (simpset() addsimps PO_simp) 1); |
400 by (simp_tac (simpset() addsimps PO_simp) 1); |
401 qed "CLF_E2"; |
401 qed "CLF_E2"; |
402 |
402 |
403 Goal "f : CLF ``` {cl} ==> f : CLF ``` {dual cl}"; |
403 Goal "f : CLF `` {cl} ==> f : CLF `` {dual cl}"; |
404 by (afs [CLF_def, CL_dualCL, monotone_dual] 1); |
404 by (afs [CLF_def, CL_dualCL, monotone_dual] 1); |
405 by (afs [dualA_iff] 1); |
405 by (afs [dualA_iff] 1); |
406 qed "CLF_dual"; |
406 qed "CLF_dual"; |
407 |
407 |
408 (* fixed points *) |
408 (* fixed points *) |