equal
deleted
inserted
replaced
129 |
129 |
130 lemma xml_of_term_code [code]: |
130 lemma xml_of_term_code [code]: |
131 "xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]" |
131 "xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]" |
132 "xml_of_term (Code_Evaluation.App t1 t2) = [xml.tagged (STR ''5'') None [xml.node (xml_of_term t1), xml.node (xml_of_term t2)]]" |
132 "xml_of_term (Code_Evaluation.App t1 t2) = [xml.tagged (STR ''5'') None [xml.node (xml_of_term t1), xml.node (xml_of_term t2)]]" |
133 "xml_of_term (Code_Evaluation.Abs x ty t) = [xml.tagged (STR ''4'') (Some x) [xml.node (xml_of_typ ty), xml.node (xml_of_term t)]]" |
133 "xml_of_term (Code_Evaluation.Abs x ty t) = [xml.tagged (STR ''4'') (Some x) [xml.node (xml_of_typ ty), xml.node (xml_of_term t)]]" |
134 (* |
134 -- {* |
135 FIXME: @{const Code_Evaluation.Free} is used only in @{theory Quickcheck_Narrowing} to represent |
135 FIXME: @{const Code_Evaluation.Free} is used only in @{theory Quickcheck_Narrowing} to represent |
136 uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables. |
136 uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables. |
137 *) |
137 *} |
138 "xml_of_term (Code_Evaluation.Free x ty) = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]" |
138 "xml_of_term (Code_Evaluation.Free x ty) = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]" |
139 by(simp_all add: xml_of_term_def xml_tree_anything) |
139 by(simp_all add: xml_of_term_def xml_tree_anything) |
140 |
140 |
141 definition yxml_string_of_term :: "Code_Evaluation.term \<Rightarrow> yxml_of_term" |
141 definition yxml_string_of_term :: "Code_Evaluation.term \<Rightarrow> yxml_of_term" |
142 where "yxml_string_of_term = yxml_string_of_body \<circ> xml_of_term" |
142 where "yxml_string_of_term = yxml_string_of_body \<circ> xml_of_term" |