changeset 71020 | 4003da7e6a79 |
parent 70915 | bd4d37edfee4 |
child 71021 | b697dd74221a |
--- a/src/HOL/Proofs/ex/XML_Data.thy Mon Nov 04 15:06:54 2019 +0100 +++ b/src/HOL/Proofs/ex/XML_Data.thy Mon Nov 04 15:14:34 2019 +0100 @@ -51,7 +51,9 @@ ML_val \<open> val xml = export_proof thy1 @{thm abs_less_iff}; val thm = import_proof thy1 xml; - \<^assert> (size (YXML.string_of_body xml) > 500000); + + val xml_size = size (YXML.string_of_body xml); + \<^assert> (xml_size > 400000); \<close> end