src/Pure/ROOT.ML
changeset 1864 9ac4c2240d89
parent 1595 b9984b1dbc4c
child 2183 8d42a7bccf0b
equal deleted inserted replaced
1863:9402e633fe53 1864:9ac4c2240d89
    10 instantiation of theorems can lead to inconsistent sorting of type vars if
    10 instantiation of theorems can lead to inconsistent sorting of type vars if
    11 'a::S is already present and 'a::T is introduced.
    11 'a::S is already present and 'a::T is introduced.
    12 *)
    12 *)
    13 
    13 
    14 val banner = "Pure Isabelle";
    14 val banner = "Pure Isabelle";
    15 val version = "Isabelle-94 revision 5: January 96";
    15 val version = "Isabelle-94 revision 6: July 96";
    16 
    16 
    17 print_depth 1;
    17 print_depth 1;
    18 
    18 
    19 use "library.ML";
    19 use "library.ML";
    20 use "symtab.ML";
    20 use "symtab.ML";