| changeset 53015 | a1119cf551e8 |
| parent 46914 | c2ca2c3d23a6 |
| child 54703 | 499f92dc6e45 |
--- a/src/HOL/Induct/Ordinals.thy Tue Aug 13 14:20:22 2013 +0200 +++ b/src/HOL/Induct/Ordinals.thy Tue Aug 13 16:25:47 2013 +0200 @@ -56,7 +56,7 @@ | "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))" definition "veb a = veblen a Zero" -definition "\<epsilon>\<^isub>0 = veb Zero" -definition "\<Gamma>\<^isub>0 = Limit (\<lambda>n. iter veb n Zero)" +definition "\<epsilon>\<^sub>0 = veb Zero" +definition "\<Gamma>\<^sub>0 = Limit (\<lambda>n. iter veb n Zero)" end