src/FOLP/ex/ROOT.ML
changeset 17480 fd19f77dcf60
parent 9000 c20d58286a51
child 25991 31b38a39e589
     1.1 --- a/src/FOLP/ex/ROOT.ML	Sat Sep 17 20:49:14 2005 +0200
     1.2 +++ b/src/FOLP/ex/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
     1.3 @@ -1,9 +1,9 @@
     1.4 -(*  Title:      FOLP/ex/ROOT
     1.5 +(*  Title:      FOLP/ex/ROOT.ML
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1992  University of Cambridge
     1.9  
    1.10 -Executes all examples for First-Order Logic. 
    1.11 +Examples for First-Order Logic. 
    1.12  *)
    1.13  
    1.14  time_use     "intro.ML";
    1.15 @@ -13,7 +13,7 @@
    1.16  writeln"\n** Intuitionistic examples **\n";
    1.17  time_use     "int.ML";
    1.18  
    1.19 -val thy = IFOLP.thy  and  tac = IntPr.fast_tac 1;
    1.20 +val thy = theory "IFOLP"  and  tac = IntPr.fast_tac 1;
    1.21  time_use     "prop.ML";
    1.22  time_use     "quant.ML";
    1.23  
    1.24 @@ -21,6 +21,6 @@
    1.25  time_use     "cla.ML";
    1.26  time_use_thy "If";
    1.27  
    1.28 -val thy = FOLP.thy  and  tac = Cla.fast_tac FOLP_cs 1;
    1.29 +val thy = theory "FOLP"  and  tac = Cla.fast_tac FOLP_cs 1;
    1.30  time_use     "prop.ML";
    1.31  time_use     "quant.ML";