| changeset 61378 | 3e04c9ca001a |
| parent 60822 | 4f58f3662e7d |
| child 61397 | 6204c86280ff |
--- a/src/ZF/Main_ZF.thy Fri Oct 09 19:51:20 2015 +0200 +++ b/src/ZF/Main_ZF.thy Fri Oct 09 20:26:03 2015 +0200 @@ -19,8 +19,6 @@ notation (xsymbols) iterates_omega ("(_^\<omega> '(_'))" [60,1000] 60) -notation (HTML output) - iterates_omega ("(_^\<omega> '(_'))" [60,1000] 60) lemma iterates_triv: "[| n\<in>nat; F(x) = x |] ==> F^n (x) = x"