changeset 20820 | 58693343905f |
parent 20801 | d3616b4abe1b |
child 21404 | eb85850d3eb7 |
--- a/src/HOL/Induct/SList.thy Sun Oct 01 22:19:21 2006 +0200 +++ b/src/HOL/Induct/SList.thy Sun Oct 01 22:19:23 2006 +0200 @@ -56,8 +56,8 @@ by (blast intro: list.NIL_I) abbreviation - "Case == Datatype_Universe.Case" - "Split == Datatype_Universe.Split" + "Case == Datatype.Case" + "Split == Datatype.Split" definition List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"