author | wenzelm |
Thu, 20 Nov 1997 16:24:05 +0100 | |
changeset 4262 | e4113a682883 |
parent 4261 | e20b9fd85811 |
child 4263 | a434327aef8b |
src/ZF/ROOT.ML | file | annotate | diff | comparison | revisions |
--- a/src/ZF/ROOT.ML Thu Nov 20 15:48:32 1997 +0100 +++ b/src/ZF/ROOT.ML Thu Nov 20 16:24:05 1997 +0100 @@ -30,7 +30,7 @@ print_depth 1; (*Add user sections for inductive/datatype definitions*) -use "../Pure/section_utils.ML"; +use "$ISABELLE_HOME/src/Pure/section_utils.ML"; use "thy_syntax.ML"; use_thy "Let";