changeset 17878 | 5b9efe4d6b47 |
parent 17248 | 81bf91654e73 |
17877:67d5ab1cb0d8 | 17878:5b9efe4d6b47 |
---|---|
1 |
|
2 (* $Id$ *) |
|
1 |
3 |
2 val asms = goal (the_context ()) "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p"; |
4 val asms = goal (the_context ()) "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p"; |
3 by (rewtac eq_def); |
5 by (rewtac eq_def); |
4 by (rtac conjI 1); |
6 by (rtac conjI 1); |
5 by (induct_tac "f" 1); |
7 by (induct_tac "f" 1); |