| changeset 55642 | 63beb38e9258 |
| parent 55575 | a5e33e18fb5c |
| child 55931 | 62156e694f3d |
--- a/src/HOL/Sum_Type.thy Fri Feb 21 00:09:55 2014 +0100 +++ b/src/HOL/Sum_Type.thy Fri Feb 21 00:09:56 2014 +0100 @@ -114,9 +114,8 @@ lemmas induct = old.sum.induct lemmas inducts = old.sum.inducts -lemmas recs = old.sum.recs -lemmas cases = sum.case -lemmas simps = sum.inject sum.distinct sum.case old.sum.recs +lemmas rec = old.sum.rec +lemmas simps = sum.inject sum.distinct sum.case sum.rec setup {* Sign.parent_path *}