| changeset 10797 | 028d22926a41 |
| parent 9969 | 4753185f1dd2 |
| child 10834 | a7897aebbffc |
--- a/src/HOL/ex/Tarski.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/ex/Tarski.ML Fri Jan 05 18:48:18 2001 +0100 @@ -400,7 +400,7 @@ by (simp_tac (simpset() addsimps PO_simp) 1); qed "CLF_E2"; -Goal "f : CLF ^^ {cl} ==> f : CLF ^^ {dual cl}"; +Goal "f : CLF ``` {cl} ==> f : CLF ``` {dual cl}"; by (afs [CLF_def, CL_dualCL, monotone_dual] 1); by (afs [dualA_iff] 1); qed "CLF_dual";