isabelle: src/ZF/ex/ROOT.ML@31847a7504ec (annotated)

0 a5a9c433f639 Initial revision clasohm parents: diff changeset	1	(* Title: ZF/ex/ROOT
a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
a5a9c433f639 Initial revision clasohm parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
a5a9c433f639 Initial revision clasohm parents: diff changeset	6	Executes all examples for Zermelo-Fraenkel Set Theory
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
16 0b033d50ca1c ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext lcp parents: 0 diff changeset	9	ZF_build_completed; (Make examples fail if ZF did)
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	10
a5a9c433f639 Initial revision clasohm parents: diff changeset	11	writeln"Root file for ZF Set Theory examples";
a5a9c433f639 Initial revision clasohm parents: diff changeset	12	proof_timing := true;
a5a9c433f639 Initial revision clasohm parents: diff changeset	13
125 bba27d15d76e changed use_thy's parameter to exact theory name clasohm parents: 120 diff changeset	14	loadpath := [".", "ex"];
bba27d15d76e changed use_thy's parameter to exact theory name clasohm parents: 120 diff changeset	15
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	16	time_use "ex/misc.ML";
125 bba27d15d76e changed use_thy's parameter to exact theory name clasohm parents: 120 diff changeset	17	time_use_thy "ex/Ramsey";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	18
540 e30c23731c2d ZF/ex/ROOT: added .ML to use command use "ex/twos_compl" lcp parents: 526 diff changeset	19	(Integers & Binary integer arithmetic)
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: 489 diff changeset	20	time_use_thy "ex/Bin";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	21
a5a9c433f639 Initial revision clasohm parents: diff changeset	22	( Datatypes )
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: 489 diff changeset	23	time_use_thy "ex/BT"; (binary trees)
526 85d7ff169b9c ZF/ex/ROOT: changed "time_use" to "time_use_thy" to load CoUnit; lcp parents: 515 diff changeset	24	time_use_thy "ex/Data"; (Sample datatype)
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: 489 diff changeset	25	time_use_thy "ex/Term"; (terms: recursion over the list functor)
abcc438e7c27 installation of new inductive/datatype sections lcp parents: 489 diff changeset	26	time_use_thy "ex/TF"; (trees/forests: mutual recursion)
489 0449a7f1add3 Addition of infinite branching datatypes lcp parents: 365 diff changeset	27	time_use_thy "ex/Ntree"; (variable-branching trees; function demo)
526 85d7ff169b9c ZF/ex/ROOT: changed "time_use" to "time_use_thy" to load CoUnit; lcp parents: 515 diff changeset	28	time_use_thy "ex/Brouwer"; (Infinite-branching trees)
180 8962c2b0dc2b ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted lcp parents: 125 diff changeset	29	time_use_thy "ex/Enum"; (Enormous enumeration type)
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	30
a5a9c433f639 Initial revision clasohm parents: diff changeset	31	( Inductive definitions )
180 8962c2b0dc2b ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted lcp parents: 125 diff changeset	32	time_use_thy "ex/Rmap"; (mapping a relation over a list)
8962c2b0dc2b ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted lcp parents: 125 diff changeset	33	time_use_thy "ex/PropLog"; (completeness of propositional logic)
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: 489 diff changeset	34	(two Coq examples by Christine Paulin-Mohring)
180 8962c2b0dc2b ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted lcp parents: 125 diff changeset	35	time_use_thy "ex/ListN";
8962c2b0dc2b ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted lcp parents: 125 diff changeset	36	time_use_thy "ex/Acc";
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: 489 diff changeset	37	time_use_thy "ex/Comb"; (Combinatory Logic example)
526 85d7ff169b9c ZF/ex/ROOT: changed "time_use" to "time_use_thy" to load CoUnit; lcp parents: 515 diff changeset	38	time_use_thy "ex/Primrec"; (Primitive recursive functions)
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	39
120 09287f26bfb8 changed all co- and co_ to co lcp parents: 95 diff changeset	40	( CoDatatypes )
76 c616d66c640e renamed some files clasohm parents: 56 diff changeset	41	time_use_thy "ex/LList";
526 85d7ff169b9c ZF/ex/ROOT: changed "time_use" to "time_use_thy" to load CoUnit; lcp parents: 515 diff changeset	42	time_use_thy "ex/CoUnit";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	43
a5a9c433f639 Initial revision clasohm parents: diff changeset	44	maketest"END: Root file for ZF Set Theory examples";

author	lcp
	Wed, 07 Sep 1994 17:28:53 +0200
changeset 589	31847a7504ec
parent 540	e30c23731c2d
child 919	49271bd72c42
permissions	-rw-r--r--