isabelle: doc-src/TutorialI/Types/ROOT.ML@ffaca9167c16 (annotated)

31678 752f23a37240 reworked section on type classes haftmann parents: 11858 diff changeset	1
752f23a37240 reworked section on type classes haftmann parents: 11858 diff changeset	2	no_document use_thy "Setup";
752f23a37240 reworked section on type classes haftmann parents: 11858 diff changeset	3
10339 ecb6eaa76843 * empty log message * nipkow parents: diff changeset	4	use "../settings.ML";
10579 1db42f739ee7 loads the new theory Numbers.thy paulson parents: 10538 diff changeset	5	use_thy "Numbers";
10538 d1bf9ca9008d * empty log message * nipkow parents: 10362 diff changeset	6	use_thy "Pairs";
11389 55e2aef8909b the records section paulson parents: 10579 diff changeset	7	use_thy "Records";
11858 ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL); wenzelm parents: 11389 diff changeset	8	use_thy "Typedefs";
31678 752f23a37240 reworked section on type classes haftmann parents: 11858 diff changeset	9	use_thy "Overloading";
10339 ecb6eaa76843 * empty log message * nipkow parents: diff changeset	10	use_thy "Axioms";