renamed CHOL to HOL
authorclasohm
Thu Jun 29 12:48:48 1995 +0200 (1995-06-29)
changeset 116597b2bb5d43c3
parent 1164 8e969adf64d6
child 1166 def4ee9e116d
renamed CHOL to HOL
src/HOL/IMP/ROOT.ML
src/HOL/Integ/ROOT.ML
src/HOL/Lambda/ROOT.ML
src/HOL/ROOT.ML
src/HOL/Subst/ROOT.ML
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IMP/ROOT.ML	Thu Jun 29 12:34:16 1995 +0200
     1.2 +++ b/src/HOL/IMP/ROOT.ML	Thu Jun 29 12:48:48 1995 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title: 	CHOL/IMP/ROOT.ML
     1.5 +(*  Title: 	HOL/IMP/ROOT.ML
     1.6      ID:         $Id$
     1.7      Author: 	Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow
     1.8      Copyright   1995 TUM
     1.9 @@ -14,9 +14,9 @@
    1.10  
    1.11  *)
    1.12  
    1.13 -CHOL_build_completed;	(*Make examples fail if CHOL did*)
    1.14 +HOL_build_completed;	(*Make examples fail if HOL did*)
    1.15  
    1.16 -writeln"Root file for CHOL/IMP";
    1.17 +writeln"Root file for HOL/IMP";
    1.18  proof_timing := true;
    1.19  loadpath := [".","IMP"];
    1.20  time_use_thy "Properties";
     2.1 --- a/src/HOL/Integ/ROOT.ML	Thu Jun 29 12:34:16 1995 +0200
     2.2 +++ b/src/HOL/Integ/ROOT.ML	Thu Jun 29 12:48:48 1995 +0200
     2.3 @@ -1,12 +1,12 @@
     2.4 -(*  Title:  	CHOL/Integ/ROOT
     2.5 +(*  Title:  	HOL/Integ/ROOT
     2.6      ID:         $Id$
     2.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     2.8      Copyright   1995  University of Cambridge
     2.9  
    2.10 -The Integers in CHOL (ported from ZF by Riccardo Mattolini)
    2.11 +The Integers in HOL (ported from ZF by Riccardo Mattolini)
    2.12  *)
    2.13  
    2.14 -CHOL_build_completed;    (*Cause examples to fail if CHOL did*)
    2.15 +HOL_build_completed;    (*Cause examples to fail if HOL did*)
    2.16  
    2.17  loadpath := ["Integ"];
    2.18  time_use_thy "Integ";
     3.1 --- a/src/HOL/Lambda/ROOT.ML	Thu Jun 29 12:34:16 1995 +0200
     3.2 +++ b/src/HOL/Lambda/ROOT.ML	Thu Jun 29 12:48:48 1995 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title: 	CHOL/IMP/ROOT.ML
     3.5 +(*  Title: 	HOL/IMP/ROOT.ML
     3.6      ID:         $Id$
     3.7      Author: 	Tobias Nipkow
     3.8      Copyright   1995 TUM
     3.9 @@ -12,8 +12,8 @@
    3.10  
    3.11  *)
    3.12  
    3.13 -CHOL_build_completed;	(*Make examples fail if CHOL did*)
    3.14 +HOL_build_completed;	(*Make examples fail if HOL did*)
    3.15  
    3.16 -writeln"Root file for CHOL/Lambda";
    3.17 +writeln"Root file for HOL/Lambda";
    3.18  loadpath := [".","Lambda"];
    3.19  time_use_thy "ParRed";
     4.1 --- a/src/HOL/ROOT.ML	Thu Jun 29 12:34:16 1995 +0200
     4.2 +++ b/src/HOL/ROOT.ML	Thu Jun 29 12:48:48 1995 +0200
     4.3 @@ -86,4 +86,4 @@
     4.4  init_pps ();
     4.5  print_depth 8;
     4.6  
     4.7 -val CHOL_build_completed = ();   (*indicate successful build*)
     4.8 +val HOL_build_completed = ();   (*indicate successful build*)
     5.1 --- a/src/HOL/Subst/ROOT.ML	Thu Jun 29 12:34:16 1995 +0200
     5.2 +++ b/src/HOL/Subst/ROOT.ML	Thu Jun 29 12:48:48 1995 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title: 	CHOL/Subst
     5.5 +(*  Title: 	HOL/Subst
     5.6      Author: 	Martin Coen, Cambridge University Computer Laboratory
     5.7      Copyright   1993  University of Cambridge
     5.8  
     5.9 @@ -22,7 +22,7 @@
    5.10  To load, go to the parent directory and type use"Subst/ROOT.ML";
    5.11  *)
    5.12  
    5.13 -CHOL_build_completed;    (*Cause examples to fail if CHOL did*)
    5.14 +HOL_build_completed;    (*Cause examples to fail if HOL did*)
    5.15  
    5.16  writeln"Root file for Substitutions and Unification";
    5.17  loadpath := ["Subst"];
     6.1 --- a/src/HOL/ex/ROOT.ML	Thu Jun 29 12:34:16 1995 +0200
     6.2 +++ b/src/HOL/ex/ROOT.ML	Thu Jun 29 12:48:48 1995 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:  	CHOL/ex/ROOT
     6.5 +(*  Title:  	HOL/ex/ROOT
     6.6      ID:         $Id$
     6.7      Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
     6.8      Copyright   1991  University of Cambridge
     6.9 @@ -6,9 +6,9 @@
    6.10  Executes miscellaneous examples for Higher-Order Logic. 
    6.11  *)
    6.12  
    6.13 -CHOL_build_completed;    (*Cause examples to fail if CHOL did*)
    6.14 +HOL_build_completed;    (*Cause examples to fail if HOL did*)
    6.15  
    6.16 -writeln "Root file for CHOL examples";
    6.17 +writeln "Root file for HOL examples";
    6.18  proof_timing := true;
    6.19  loadpath := ["ex"];
    6.20  time_use     "ex/cla.ML";
    6.21 @@ -28,4 +28,4 @@
    6.22  time_use_thy "Term";
    6.23  time_use_thy "Simult";
    6.24  time_use_thy "MT";
    6.25 -writeln "END: Root file for CHOL examples";
    6.26 +writeln "END: Root file for HOL examples";