changeset 28524 | 644b62cf678f |
parent 28346 | b8390cd56b8f |
child 28562 | 4e74209f113e |
--- a/src/HOL/Datatype.thy Tue Oct 07 16:07:40 2008 +0200 +++ b/src/HOL/Datatype.thy Tue Oct 07 16:07:50 2008 +0200 @@ -567,10 +567,10 @@ constdefs Suml :: "('a => 'c) => 'a + 'b => 'c" - "Suml == (%f. sum_case f arbitrary)" + "Suml == (%f. sum_case f undefined)" Sumr :: "('b => 'c) => 'a + 'b => 'c" - "Sumr == sum_case arbitrary" + "Sumr == sum_case undefined" lemma Suml_inject: "Suml f = Suml g ==> f = g" by (unfold Suml_def) (erule sum_case_inject)