--- a/src/HOL/String.thy Thu Sep 09 11:10:44 2010 +0200
+++ b/src/HOL/String.thy Thu Sep 09 14:38:14 2010 +0200
@@ -152,18 +152,36 @@
Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
-subsection {* Strings as dedicated datatype *}
+subsection {* Strings as dedicated type *}
+
+typedef (open) literal = "UNIV :: string \<Rightarrow> bool"
+ morphisms explode STR ..
+
+code_datatype STR
-datatype literal = STR string
+instantiation literal :: size
+begin
-declare literal.cases [code del] literal.recs [code del]
+definition size_literal :: "literal \<Rightarrow> nat"
+where
+ [code]: "size_literal (s\<Colon>literal) = 0"
-lemma [code]: "size (s\<Colon>literal) = 0"
- by (cases s) simp_all
+instance ..
+
+end
+
+instantiation literal :: equal
+begin
-lemma [code]: "literal_size (s\<Colon>literal) = 0"
- by (cases s) simp_all
+definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
+where
+ "equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
+instance
+proof
+qed (auto simp add: equal_literal_def explode_inject)
+
+end
subsection {* Code generator *}
@@ -231,4 +249,4 @@
code_modulename Haskell
String String
-end
\ No newline at end of file
+end