equal
deleted
inserted
replaced
140 definition yxml_string_of_term :: "Code_Evaluation.term \<Rightarrow> yxml_of_term" |
140 definition yxml_string_of_term :: "Code_Evaluation.term \<Rightarrow> yxml_of_term" |
141 where "yxml_string_of_term = yxml_string_of_body \<circ> xml_of_term" |
141 where "yxml_string_of_term = yxml_string_of_body \<circ> xml_of_term" |
142 |
142 |
143 subsection \<open>Test engine and drivers\<close> |
143 subsection \<open>Test engine and drivers\<close> |
144 |
144 |
145 ML_file "code_test.ML" |
145 ML_file \<open>code_test.ML\<close> |
146 |
146 |
147 end |
147 end |