isabelle: src/HOL/Induct/ROOT.ML@90d03908b3d7 (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
28385 74c6d73a8b2e setmp_noncritical; wenzelm parents: 24607 diff changeset	4	setmp_noncritical quick_and_dirty true
24607 fc06b84acd81 added Induct/Common_Patterns.thy; wenzelm parents: 24104 diff changeset	5	use_thy "Common_Patterns";
fc06b84acd81 added Induct/Common_Patterns.thy; wenzelm parents: 24104 diff changeset	6
28827 b3ce1912ac25 removed Induct/Mutil.thy -- the file has been moved to AFP; wenzelm parents: 28385 diff changeset	7	use_thys ["QuoDataType", "QuoNestedDataType", "Term",
24104 719fbe4fb77f simultaneous use_thys; wenzelm parents: 23746 diff changeset	8	"ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog",
719fbe4fb77f simultaneous use_thys; wenzelm parents: 23746 diff changeset	9	"SList", "LFilter", "Com"];