| changeset 17248 | 81bf91654e73 |
| parent 4905 | be73ddff6c5a |
| child 17878 | 5b9efe4d6b47 |
--- a/src/LCF/ex/Ex4.ML Sat Sep 03 17:54:07 2005 +0200 +++ b/src/LCF/ex/Ex4.ML Sat Sep 03 17:54:10 2005 +0200 @@ -1,5 +1,5 @@ -val asms = goal thy "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p"; +val asms = goal (the_context ()) "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p"; by (rewtac eq_def); by (rtac conjI 1); by (induct_tac "f" 1);