doc-src/TutorialI/Types/ROOT.ML
changeset 11858 ca128c9100b6
parent 11389 55e2aef8909b
child 31678 752f23a37240
equal deleted inserted replaced
11857:cc3d971fe66a 11858:ca128c9100b6
     1 (* ID:         $Id$ *)
     1 (* ID:         $Id$ *)
     2 use "../settings.ML";
     2 use "../settings.ML";
     3 use_thy "Numbers";
     3 use_thy "Numbers";
     4 use_thy "Pairs";
     4 use_thy "Pairs";
     5 use_thy "Records";
     5 use_thy "Records";
     6 use_thy "Typedef";
     6 use_thy "Typedefs";
     7 use_thy "Overloading0";
     7 use_thy "Overloading0";
     8 use_thy "Overloading2";
     8 use_thy "Overloading2";
     9 use_thy "Axioms";
     9 use_thy "Axioms";