isabelle: Admin/Benchmarks/HOL-datatype/ROOT.ML@5584ab3d5b13 (annotated)

7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	1	(* Title: Admin/Benchmarks/HOL-datatype/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
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	6	val tests = ["Brackin", "Instructions", "SML", "Verilog"];
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	7
32871 36fa392ba61a explicitly unsynchronized haftmann parents: 32870 diff changeset	8	Unsynchronized.set timing;
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	9
32870 e23a35f5400d explicitly unsynchronized haftmann parents: 27641 diff changeset	10	warning "\nset quick_and_dirty\n"; Unsynchronized.set quick_and_dirty;
37875 496d723516e6 recovered benchmarks, which are not tested automatically; wenzelm parents: 32871 diff changeset	11	use_thys tests;
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	12
32870 e23a35f5400d explicitly unsynchronized haftmann parents: 27641 diff changeset	13	warning "\nreset quick_and_dirty\n"; Unsynchronized.reset quick_and_dirty;
37875 496d723516e6 recovered benchmarks, which are not tested automatically; wenzelm parents: 32871 diff changeset	14	List.app Thy_Info.remove_thy tests;
496d723516e6 recovered benchmarks, which are not tested automatically; wenzelm parents: 32871 diff changeset	15	use_thys tests;

author	wenzelm
	Fri, 13 Aug 2010 18:16:50 +0200
changeset 38369	5584ab3d5b13
parent 37875	496d723516e6
child 38798	89f273ab1d42
permissions	-rw-r--r--