| changeset 60157 | ccf9241af217 |
| parent 58372 | bfd497f2f4c2 |
| child 60360 | f585b1f0b4c3 |
| 60156:76853162a87e | 60157:ccf9241af217 |
|---|---|
55 *} |
55 *} |
56 |
56 |
57 text {* Some fairly large proof: *} |
57 text {* Some fairly large proof: *} |
58 |
58 |
59 ML_val {* |
59 ML_val {* |
60 val xml = export_proof @{thm Int.times_int.abs_eq}; |
60 val xml = export_proof @{thm abs_less_iff}; |
61 val thm = import_proof thy1 xml; |
61 val thm = import_proof thy1 xml; |
62 @{assert} (size (YXML.string_of_body xml) > 50000000); |
62 @{assert} (size (YXML.string_of_body xml) > 1000000); |
63 *} |
63 *} |
64 |
64 |
65 end |
65 end |