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

9000 c20d58286a51 cleaned up; wenzelm parents: 6349 diff changeset	1	(* Title: CTT/ex/ROOT.ML
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
a5a9c433f639 Initial revision clasohm parents: diff changeset	9	print_depth 2;
4446 097004a470fb tuned; wenzelm parents: 2822 diff changeset	10
2822 50bac845de6f exit_use_dir; wenzelm parents: 1459 diff changeset	11	time_use "typechk.ML";
50bac845de6f exit_use_dir; wenzelm parents: 1459 diff changeset	12	time_use "elim.ML";
50bac845de6f exit_use_dir; wenzelm parents: 1459 diff changeset	13	time_use "equal.ML";
50bac845de6f exit_use_dir; wenzelm parents: 1459 diff changeset	14	time_use "synth.ML";