author | haftmann |
Thu, 28 Feb 2008 16:54:56 +0100 | |
changeset 26183 | 0cc3ff184282 |
parent 26182 | 8262ec0e8782 |
child 26184 | 64ee6a2ca6d6 |
--- a/src/HOL/Library/RType.thy Thu Feb 28 16:50:52 2008 +0100 +++ b/src/HOL/Library/RType.thy Thu Feb 28 16:54:56 2008 +0100 @@ -6,7 +6,7 @@ header {* Reflecting Pure types into HOL *} theory RType -imports Main Code_Message +imports Main Code_Message Code_Index (* import all 'special code' types *) begin datatype "rtype" = RType message_string "rtype list"