src/Pure/ROOT.ML
changeset 1072 0140ff702b23
parent 922 196ca0973a6d
child 1078 e57beb974dd7
equal deleted inserted replaced
1071:96dfc9977bf5 1072:0140ff702b23
    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 3: March 95";
    15 val version = "Isabelle-94 revision 3: April 95";
    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";