equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Reflecting Pure types into HOL *} |
6 header {* Reflecting Pure types into HOL *} |
7 |
7 |
8 theory RType |
8 theory RType |
9 imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Message" "~~/src/HOL/Code_Index" (* import all 'special code' types *) |
9 imports Plain "~~/src/HOL/List" "~~/src/HOL/Library/Code_Message" |
10 begin |
10 begin |
11 |
11 |
12 datatype "rtype" = RType message_string "rtype list" |
12 datatype "rtype" = RType message_string "rtype list" |
13 |
13 |
14 class rtype = |
14 class rtype = |