isabelle: src/LCF/ex/ROOT.ML@6303966dce96 (annotated)

2820 6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	1
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	2	writeln"Root file for LCF examples";
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	3	LCF_build_completed; (Cause examples to fail if LCF did)
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	4
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	5	proof_timing := true;
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	6
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	7	use"ex.ML";
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	8
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	9	cd "..";
6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	10	maketest"END: file for LCF examples";