isabelle: src/Cube/ex/ROOT.ML@23564e91463e (annotated)

2817 23564e91463e replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	1
23564e91463e replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	2	writeln"Root file for Cube examples";
23564e91463e replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	3	Cube_build_completed; (Cause examples to fail if Cube did)
23564e91463e replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	4
23564e91463e replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	5	proof_timing := true;
23564e91463e replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	6
23564e91463e replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	7	use"ex.ML";
23564e91463e replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	8
23564e91463e replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	9	cd "..";
23564e91463e replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	10	maketest"END: file for Lambda-Cube examples";