isabelle: Admin/Benchmarks/HOL-datatype/ROOT.ML@b0d2b49bfaed (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	ID: $Id$
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	3
15661 9ef583b08647 reverted renaming of Some/None in comments and strings; wenzelm parents: 15531 diff changeset	4	Some rather large datatype examples (from John Harrison).
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	5	*)
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	6
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	7	val tests = ["Brackin", "Instructions", "SML", "Verilog"];
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	8
9000 c20d58286a51 cleaned up; wenzelm parents: 7373 diff changeset	9	set timing;
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	10
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	11	warning "\nset quick_and_dirty\n"; set quick_and_dirty;
16692 d3416641926f List.app; wenzelm parents: 15661 diff changeset	12	List.app time_use_thy tests;
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	13
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	14	warning "\nreset quick_and_dirty\n"; reset quick_and_dirty;
27641 4d7c96b72d49 ThyInfo.remove_thy; wenzelm parents: 16692 diff changeset	15	List.app ThyInfo.remove_thy tests;
16692 d3416641926f List.app; wenzelm parents: 15661 diff changeset	16	List.app time_use_thy tests;

author	haftmann
	Fri, 14 Aug 2009 15:36:54 +0200
changeset 32372	b0d2b49bfaed
parent 27641	4d7c96b72d49
child 32870	e23a35f5400d
permissions	-rw-r--r--