isabelle: src/CTT/ex/ROOT.ML@6a65e9b2ae05 (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
19761 5cd82054c2c6 removed obsolete ML files; wenzelm parents: 9000 diff changeset	6	Examples for Constructive Type Theory.
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
19761 5cd82054c2c6 removed obsolete ML files; wenzelm parents: 9000 diff changeset	9	use_thy "Typechecking";
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 9000 diff changeset	10	use_thy "Elimination";
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 9000 diff changeset	11	use_thy "Equality";
5cd82054c2c6 removed obsolete ML files; wenzelm parents: 9000 diff changeset	12	use_thy "Synthesis";