| changeset 6382 | 8b0c9205da75 |
| parent 5977 | 9f0c8869cf71 |
| child 10834 | a7897aebbffc |
--- a/src/HOL/Induct/LList.thy Wed Mar 17 13:47:04 1999 +0100 +++ b/src/HOL/Induct/LList.thy Wed Mar 17 13:47:34 1999 +0100 @@ -44,7 +44,7 @@ typedef (LList) - 'a llist = "llist(range Leaf)" (llist.NIL_I) + 'a llist = "llist(range Leaf) :: 'a item set" (llist.NIL_I) constdefs (*Now used exclusively for abbreviating the coinduction rule*)