isabelle: src/CTT/ex/ROOT.ML@a79d4683fadf (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
a5a9c433f639 Initial revision clasohm parents: diff changeset	11	print_depth 2;
4446 097004a470fb tuned; wenzelm parents: 2822 diff changeset	12	set proof_timing;
097004a470fb tuned; wenzelm parents: 2822 diff changeset	13
2822 50bac845de6f exit_use_dir; wenzelm parents: 1459 diff changeset	14	time_use "typechk.ML";
50bac845de6f exit_use_dir; wenzelm parents: 1459 diff changeset	15	time_use "elim.ML";
50bac845de6f exit_use_dir; wenzelm parents: 1459 diff changeset	16	time_use "equal.ML";
50bac845de6f exit_use_dir; wenzelm parents: 1459 diff changeset	17	time_use "synth.ML";

author	wenzelm
	Thu, 26 Aug 1999 19:01:58 +0200
changeset 7367	a79d4683fadf
parent 6349	f7750d816c21
child 9000	c20d58286a51
permissions	-rw-r--r--