diff -r 3667b4616e9a -r c6dc17aab88a src/ZF/Main.thy --- 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" ("(_^\ '(_'))" [60,1000] 60) +syntax (HTML output) + iterates_omega :: "[i=>i,i] => i" ("(_^\ '(_'))" [60,1000] 60) lemma iterates_triv: "[| n\nat; F(x) = x |] ==> F^n (x) = x"