src/Pure/ROOT.ML
changeset 83 de9316670e89
parent 73 075db6ac7f2f
child 403 4c66b1577753
equal deleted inserted replaced
82:b9ac34abc054 83:de9316670e89
    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 = "February 93";
    15 val version = "October 93";
    16 
    16 
    17 print_depth 1;
    17 print_depth 1;
    18 
    18 
    19 use "library.ML";
    19 use "library.ML";
    20 use "term.ML";
    20 use "term.ML";