src/CTT/ROOT.ML
changeset 1459 d12da312eff4
parent 1361 90d615b599d9
child 2237 f01ac387e82b
equal deleted inserted replaced
1458:fd510875fb71 1459:d12da312eff4
     1 (*  Title: 	CTT/ROOT
     1 (*  Title:      CTT/ROOT
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     4     Copyright   1991  University of Cambridge
     5 
     5 
     6 Adds Constructive Type Theory to a database containing pure Isabelle. 
     6 Adds Constructive Type Theory to a database containing pure Isabelle. 
     7 Should be executed in the subdirectory CTT.
     7 Should be executed in the subdirectory CTT.
     8 *)
     8 *)
    21 use_thy "Bool";
    21 use_thy "Bool";
    22 
    22 
    23 use "../Pure/install_pp.ML";
    23 use "../Pure/install_pp.ML";
    24 print_depth 8;
    24 print_depth 8;
    25 
    25 
    26 val CTT_build_completed = ();	(*indicate successful build*)
    26 val CTT_build_completed = ();   (*indicate successful build*)