isabelle: src/CTT/ex/ROOT.ML@c04027ccc86e (annotated)

1459 d12da312eff4 expanded tabs clasohm parents: 1352 diff changeset	1	(* Title: CTT/ex/ROOT
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1459 d12da312eff4 expanded tabs clasohm parents: 1352 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1991 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
a5a9c433f639 Initial revision clasohm parents: diff changeset	6	Executes all examples for Constructive Type Theory.
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
2822 50bac845de6f exit_use_dir; wenzelm parents: 1459 diff changeset	9	writeln"Root file for CTT examples";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	10
2822 50bac845de6f exit_use_dir; wenzelm parents: 1459 diff changeset	11	CTT_build_completed; (Cause examples to fail if CTT did)
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	12
a5a9c433f639 Initial revision clasohm parents: diff changeset	13	print_depth 2;
4446 097004a470fb tuned; wenzelm parents: 2822 diff changeset	14	set proof_timing;
097004a470fb tuned; wenzelm parents: 2822 diff changeset	15
2822 50bac845de6f exit_use_dir; wenzelm parents: 1459 diff changeset	16	time_use "typechk.ML";
50bac845de6f exit_use_dir; wenzelm parents: 1459 diff changeset	17	time_use "elim.ML";
50bac845de6f exit_use_dir; wenzelm parents: 1459 diff changeset	18	time_use "equal.ML";
50bac845de6f exit_use_dir; wenzelm parents: 1459 diff changeset	19	time_use "synth.ML";

author	wenzelm
	Wed, 14 Jan 1998 10:30:01 +0100
changeset 4570	c04027ccc86e
parent 4446	097004a470fb
child 6349	f7750d816c21
permissions	-rw-r--r--