changeset 36176 | 3fe7e97ccca8 |
parent 35123 | e286d5df187a |
child 37742 | 0a3fa8fbcdc5 |
1.1 --- a/src/HOL/String.thy Fri Apr 16 20:56:40 2010 +0200 1.2 +++ b/src/HOL/String.thy Fri Apr 16 21:28:09 2010 +0200 1.3 @@ -217,6 +217,6 @@ 1.4 in Codegen.add_codegen "char_codegen" char_codegen end 1.5 *} 1.6 1.7 -hide (open) type literal 1.8 +hide_type (open) literal 1.9 1.10 end 1.11 \ No newline at end of file