| changeset 46954 | d8b3412cdb99 |
| parent 46953 | 2b6e55924af3 |
| child 46993 | 7371429c527d |
--- a/src/ZF/Ordinal.thy Thu Mar 15 16:35:02 2012 +0000 +++ b/src/ZF/Ordinal.thy Thu Mar 15 17:38:05 2012 +0000 @@ -703,7 +703,7 @@ lemma Ord_cases: assumes i: "Ord(i)" - obtains (0) "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)" + obtains ("0") "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)" by (insert Ord_cases_disj [OF i], auto) lemma trans_induct3_raw: