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

3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	1
11046 b5f5942781a0 Induct: converted some theories to new-style format; wenzelm parents: 10876 diff changeset	2	time_use_thy "Mutil";
b5f5942781a0 Induct: converted some theories to new-style format; wenzelm parents: 10876 diff changeset	3	time_use_thy "Term";
b5f5942781a0 Induct: converted some theories to new-style format; wenzelm parents: 10876 diff changeset	4	time_use_thy "ABexp";
b5f5942781a0 Induct: converted some theories to new-style format; wenzelm parents: 10876 diff changeset	5	time_use_thy "Tree";
11641 0c248bed5225 added Ordinals example; wenzelm parents: 11058 diff changeset	6	time_use_thy "Ordinals";
10876 e12892e4666a added Sigma_Algebra; wenzelm parents: 10566 diff changeset	7	time_use_thy "Sigma_Algebra";
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	8	time_use_thy "Comb";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	9	time_use_thy "PropLog";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	10	time_use_thy "SList";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	11	time_use_thy "LFilter";
14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 13075 diff changeset	12
d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 13075 diff changeset	13	time_use_thy "BinaryTree_Map";
d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 13075 diff changeset	14	time_use_thy "BinaryTree_TacticStyle";

author	paulson
	Fri, 19 Mar 2004 10:42:38 +0100
changeset 14472	cba7c0a3ffb3
parent 14288	d149e3cbdb39
child 14505	e2373489d373
permissions	-rw-r--r--