isabelle: src/HOL/Datatype_Benchmark/ROOT.ML@63c05991882e (annotated)

45860 93eda35a8377 more visible benchmarks; wenzelm parents: 44639 diff changeset	1	(* Title: HOL/Datatype_Benchmark/ROOT.ML
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	2
15661 9ef583b08647 reverted renaming of Some/None in comments and strings; wenzelm parents: 15531 diff changeset	3	Some rather large datatype examples (from John Harrison).
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	4	*)
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	5
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	6	Toplevel.timing := true;
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	7
45860 93eda35a8377 more visible benchmarks; wenzelm parents: 44639 diff changeset	8	use_thys ["Brackin", "Instructions", "SML", "Verilog"];