src/LCF/ROOT.ML
changeset 25750 4e796867ccb5
parent 17247 6927a62c77dc
child 33615 261abc2e3155
equal deleted inserted replaced
25749:10e7feb4e595 25750:4e796867ccb5
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     3     Author:     Tobias Nipkow
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 *)
     5 *)
     6 
     6 
     7 val banner = "Logic for Computable Functions (in FOL)";
     7 use_thy "LCF";
     8 writeln banner;
       
     9 
     8 
    10 use_thy "LCF";