--- a/src/HOL/String.thy Sat Oct 20 09:09:37 2012 +0200
+++ b/src/HOL/String.thy Sat Oct 20 09:12:16 2012 +0200
@@ -149,6 +149,14 @@
Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
+lemma UNIV_set_chars:
+ "UNIV = set chars"
+ by (simp only: UNIV_char UNIV_nibble) code_simp
+
+lemma distinct_chars:
+ "distinct chars"
+ by code_simp
+
subsection {* Strings as dedicated type *}
@@ -213,3 +221,4 @@
hide_type (open) literal
end
+