equal
deleted
inserted
replaced
124 |
124 |
125 syntax |
125 syntax |
126 "_String" :: "str_position => string" ("_") |
126 "_String" :: "str_position => string" ("_") |
127 |
127 |
128 ML_file "Tools/string_syntax.ML" |
128 ML_file "Tools/string_syntax.ML" |
129 setup String_Syntax.setup |
|
130 |
129 |
131 lemma UNIV_char: |
130 lemma UNIV_char: |
132 "UNIV = image (split Char) (UNIV \<times> UNIV)" |
131 "UNIV = image (split Char) (UNIV \<times> UNIV)" |
133 proof (rule UNIV_eq_I) |
132 proof (rule UNIV_eq_I) |
134 fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto |
133 fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto |