changeset 14565 | c6dc17aab88a |
parent 13694 | be3e2fa01b0f |
child 16417 | 9bc16273c2d4 |
--- a/src/ZF/Main.thy Wed Apr 14 13:28:46 2004 +0200 +++ b/src/ZF/Main.thy Wed Apr 14 14:13:05 2004 +0200 @@ -21,6 +21,8 @@ syntax (xsymbols) iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60) +syntax (HTML output) + iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60) lemma iterates_triv: "[| n\<in>nat; F(x) = x |] ==> F^n (x) = x"