isabelle: src/HOL/Induct/ROOT.ML@7540ccd2b445 (annotated)

17598 7540ccd2b445 Id; wenzelm parents: 15172 diff changeset	1
7540ccd2b445 Id; wenzelm parents: 15172 diff changeset	2	(* $Id$ *)
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	3
11046 b5f5942781a0 Induct: converted some theories to new-style format; wenzelm parents: 10876 diff changeset	4	time_use_thy "Mutil";
14527 bc9e5587d05a IsaMakefile paulson parents: 14505 diff changeset	5	time_use_thy "QuoDataType";
15172 73069e033a0b new example of a quotiented nested data type paulson parents: 14527 diff changeset	6	time_use_thy "QuoNestedDataType";
11046 b5f5942781a0 Induct: converted some theories to new-style format; wenzelm parents: 10876 diff changeset	7	time_use_thy "Term";
b5f5942781a0 Induct: converted some theories to new-style format; wenzelm parents: 10876 diff changeset	8	time_use_thy "ABexp";
b5f5942781a0 Induct: converted some theories to new-style format; wenzelm parents: 10876 diff changeset	9	time_use_thy "Tree";
11641 0c248bed5225 added Ordinals example; wenzelm parents: 11058 diff changeset	10	time_use_thy "Ordinals";
10876 e12892e4666a added Sigma_Algebra; wenzelm parents: 10566 diff changeset	11	time_use_thy "Sigma_Algebra";
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	12	time_use_thy "Comb";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	13	time_use_thy "PropLog";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	14	time_use_thy "SList";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	15	time_use_thy "LFilter";

author	wenzelm
	Fri, 23 Sep 2005 14:55:28 +0200
changeset 17598	7540ccd2b445
parent 15172	73069e033a0b
child 23746	a455e69c31cc
permissions	-rw-r--r--