$ISABELLE_HOME/src;
authorwenzelm
Thu Nov 20 16:24:05 1997 +0100 (1997-11-20)
changeset 4262e4113a682883
parent 4261 e20b9fd85811
child 4263 a434327aef8b
$ISABELLE_HOME/src;
src/ZF/ROOT.ML
     1.1 --- a/src/ZF/ROOT.ML	Thu Nov 20 15:48:32 1997 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Thu Nov 20 16:24:05 1997 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4  print_depth 1;
     1.5  
     1.6  (*Add user sections for inductive/datatype definitions*)
     1.7 -use     "../Pure/section_utils.ML";
     1.8 +use     "$ISABELLE_HOME/src/Pure/section_utils.ML";
     1.9  use     "thy_syntax.ML";
    1.10  
    1.11  use_thy "Let";