refer to $ISABELLE_HOME/src;
authorwenzelm
Wed Nov 12 16:28:53 1997 +0100 (1997-11-12)
changeset 4222d7573d6d0513
parent 4221 ed0f67fb458b
child 4223 f60e3d2c81d3
refer to $ISABELLE_HOME/src;
src/CTT/ROOT.ML
src/FOL/ROOT.ML
src/HOL/ROOT.ML
     1.1 --- a/src/CTT/ROOT.ML	Wed Nov 12 16:27:13 1997 +0100
     1.2 +++ b/src/CTT/ROOT.ML	Wed Nov 12 16:28:53 1997 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4  print_depth 1;  
     1.5  
     1.6  use_thy "CTT";
     1.7 -use "../Provers/typedsimp.ML";
     1.8 +use "$ISABELLE_HOME/src/Provers/typedsimp.ML";
     1.9  use "rew.ML";
    1.10  use_thy "Arith";
    1.11  use_thy "Bool";
     2.1 --- a/src/FOL/ROOT.ML	Wed Nov 12 16:27:13 1997 +0100
     2.2 +++ b/src/FOL/ROOT.ML	Wed Nov 12 16:28:53 1997 +0100
     2.3 @@ -13,12 +13,12 @@
     2.4  
     2.5  print_depth 1;  
     2.6  
     2.7 -use "../Provers/simplifier.ML";
     2.8 -use "../Provers/splitter.ML";
     2.9 -use "../Provers/ind.ML";
    2.10 -use "../Provers/hypsubst.ML";
    2.11 -use "../Provers/classical.ML";
    2.12 -use "../Provers/blast.ML";
    2.13 +use "$ISABELLE_HOME/src/Provers/simplifier.ML";
    2.14 +use "$ISABELLE_HOME/src/Provers/splitter.ML";
    2.15 +use "$ISABELLE_HOME/src/Provers/ind.ML";
    2.16 +use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
    2.17 +use "$ISABELLE_HOME/src/Provers/classical.ML";
    2.18 +use "$ISABELLE_HOME/src/Provers/blast.ML";
    2.19  
    2.20  use_thy "IFOL";
    2.21  
     3.1 --- a/src/HOL/ROOT.ML	Wed Nov 12 16:27:13 1997 +0100
     3.2 +++ b/src/HOL/ROOT.ML	Wed Nov 12 16:28:53 1997 +0100
     3.3 @@ -13,15 +13,15 @@
     3.4  print_depth 1;
     3.5  
     3.6  (* Add user sections *)
     3.7 -use "../Pure/section_utils.ML";
     3.8 +use "$ISABELLE_HOME/src/Pure/section_utils.ML";
     3.9  use "thy_syntax.ML";
    3.10  
    3.11 -use "../Provers/simplifier.ML";
    3.12 -use "../Provers/splitter.ML";
    3.13 -use "../Provers/hypsubst.ML";
    3.14 -use "../Provers/classical.ML";
    3.15 -use "../Provers/blast.ML";
    3.16 -use "../Provers/nat_transitive.ML";
    3.17 +use "$ISABELLE_HOME/src/Provers/simplifier.ML";
    3.18 +use "$ISABELLE_HOME/src/Provers/splitter.ML";
    3.19 +use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
    3.20 +use "$ISABELLE_HOME/src/Provers/classical.ML";
    3.21 +use "$ISABELLE_HOME/src/Provers/blast.ML";
    3.22 +use "$ISABELLE_HOME/src/Provers/nat_transitive.ML";
    3.23  
    3.24  use "thy_data.ML";
    3.25  
    3.26 @@ -32,7 +32,7 @@
    3.27  
    3.28  use_thy "Ord";
    3.29  use_thy "subset";
    3.30 -use     "typedef.ML";
    3.31 +use "typedef.ML";
    3.32  use_thy "Sum";
    3.33  use_thy "Gfp";
    3.34