| changeset 60157 | ccf9241af217 |
| parent 58372 | bfd497f2f4c2 |
| child 60360 | f585b1f0b4c3 |
--- a/src/HOL/Proofs/ex/XML_Data.thy Wed Apr 29 23:26:11 2015 +0200 +++ b/src/HOL/Proofs/ex/XML_Data.thy Wed Apr 29 23:30:47 2015 +0200 @@ -57,9 +57,9 @@ text {* Some fairly large proof: *} ML_val {* - val xml = export_proof @{thm Int.times_int.abs_eq}; + val xml = export_proof @{thm abs_less_iff}; val thm = import_proof thy1 xml; - @{assert} (size (YXML.string_of_body xml) > 50000000); + @{assert} (size (YXML.string_of_body xml) > 1000000); *} end