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

9450 c97dba47e504 tuned; wenzelm parents: 9000 diff changeset	1	(* Title: HOL/Induct/ROOT.ML
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	2
9450 c97dba47e504 tuned; wenzelm parents: 9000 diff changeset	3	Examples of Inductive and Coinductive Definitions.
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	4	*)
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	5
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	6	time_use_thy "Perm";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	7	time_use_thy "Comb";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	8	time_use_thy "Mutil";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	9	time_use_thy "Acc";
8917 2ff6f8693c4f loading the new theory MultisetOrder paulson parents: 7019 diff changeset	10	time_use_thy "MultisetOrder";
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	11	time_use_thy "PropLog";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	12	time_use_thy "SList";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	13	time_use_thy "LFilter";
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	14	time_use_thy "Term";
5739 f35761a1e1c4 Added new theory ABexp, removed obsolete theory Simult. berghofe parents: 5628 diff changeset	15	time_use_thy "ABexp";
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	16	time_use_thy "Exp";
7019 71f2155cdd85 Added new example (infinitely branching trees). berghofe parents: 6349 diff changeset	17	time_use_thy "Tree";

author	wenzelm
	Thu, 27 Jul 2000 18:23:12 +0200
changeset 9450	c97dba47e504
parent 9000	c20d58286a51
child 9951	5610c4acb48d
permissions	-rw-r--r--