src/HOL/Library/Code_Test.thy
changeset 62597 b3f2b8c906a6
parent 61585 a9599d3d7610
child 63680 6e1e8b5abbfa
--- a/src/HOL/Library/Code_Test.thy	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/Library/Code_Test.thy	Sat Mar 12 22:04:52 2016 +0100
@@ -83,8 +83,8 @@
 
 definition list where "list f xs = map (node \<circ> f) xs"
 
-definition X :: yxml_of_term where "X = yot_literal (STR [Char Nibble0 Nibble5])"
-definition Y :: yxml_of_term where "Y = yot_literal (STR [Char Nibble0 Nibble6])"
+definition X :: yxml_of_term where "X = yot_literal (STR [Char (num.Bit1 (num.Bit0 num.One))])"
+definition Y :: yxml_of_term where "Y = yot_literal (STR [Char (num.Bit0 (num.Bit1 num.One))])"
 definition XY :: yxml_of_term where "XY = yot_append X Y"
 definition XYX :: yxml_of_term where "XYX = yot_append XY X"