isabelle: src/HOL/Induct/ROOT.ML@b84f3c3c27f2 (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
24607 fc06b84acd81 added Induct/Common_Patterns.thy; wenzelm parents: 24104 diff changeset	4	setmp quick_and_dirty true
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
24104 719fbe4fb77f simultaneous use_thys; wenzelm parents: 23746 diff changeset	7	use_thys ["Mutil", "QuoDataType", "QuoNestedDataType", "Term",
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"];