| changeset 6382 | 8b0c9205da75 |
| parent 5977 | 9f0c8869cf71 |
| child 11481 | c77e5401f2ff |
--- a/src/HOL/Induct/SList.thy Wed Mar 17 13:47:04 1999 +0100 +++ b/src/HOL/Induct/SList.thy Wed Mar 17 13:47:34 1999 +0100 @@ -33,7 +33,7 @@ typedef (List) - 'a list = "list(range Leaf)" (list.NIL_I) + 'a list = "list(range Leaf) :: 'a item set" (list.NIL_I) (*Declaring the abstract list constructors*)