equal
deleted
inserted
replaced
81 definition tagged :: "String.literal \<Rightarrow> String.literal option \<Rightarrow> xml_tree list \<Rightarrow> xml_tree" |
81 definition tagged :: "String.literal \<Rightarrow> String.literal option \<Rightarrow> xml_tree list \<Rightarrow> xml_tree" |
82 where "tagged tag x ts = Elem tag (case x of None \<Rightarrow> [] | Some x' \<Rightarrow> [(STR ''0'', x')]) ts" |
82 where "tagged tag x ts = Elem tag (case x of None \<Rightarrow> [] | Some x' \<Rightarrow> [(STR ''0'', x')]) ts" |
83 |
83 |
84 definition list where "list f xs = map (node \<circ> f) xs" |
84 definition list where "list f xs = map (node \<circ> f) xs" |
85 |
85 |
86 definition X :: yxml_of_term where "X = yot_literal (STR [Char Nibble0 Nibble5])" |
86 definition X :: yxml_of_term where "X = yot_literal (STR [Char (num.Bit1 (num.Bit0 num.One))])" |
87 definition Y :: yxml_of_term where "Y = yot_literal (STR [Char Nibble0 Nibble6])" |
87 definition Y :: yxml_of_term where "Y = yot_literal (STR [Char (num.Bit0 (num.Bit1 num.One))])" |
88 definition XY :: yxml_of_term where "XY = yot_append X Y" |
88 definition XY :: yxml_of_term where "XY = yot_append X Y" |
89 definition XYX :: yxml_of_term where "XYX = yot_append XY X" |
89 definition XYX :: yxml_of_term where "XYX = yot_append XY X" |
90 |
90 |
91 end |
91 end |
92 |
92 |