equal
deleted
inserted
replaced
233 |
233 |
234 text {* Here are some bigger examples for benchmarking. *} |
234 text {* Here are some bigger examples for benchmarking. *} |
235 |
235 |
236 ML {* |
236 ML {* |
237 fun make_benchmark n = |
237 fun make_benchmark n = |
238 writeln (Markup.markup Markup.sendback |
238 writeln (Markup.markup Isabelle_Markup.sendback |
239 ("statespace benchmark" ^ string_of_int n ^ " =\n" ^ |
239 ("statespace benchmark" ^ string_of_int n ^ " =\n" ^ |
240 (cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n))))); |
240 (cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n))))); |
241 *} |
241 *} |
242 |
242 |
243 text "0.2s" |
243 text "0.2s" |