equal
deleted
inserted
replaced
29 echo " -u pass 'use\"ROOT.ML\";' to the ML session" |
29 echo " -u pass 'use\"ROOT.ML\";' to the ML session" |
30 echo " -w reset write permissions on OUTPUT" |
30 echo " -w reset write permissions on OUTPUT" |
31 echo |
31 echo |
32 echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps." |
32 echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps." |
33 echo " These are either names to be searched in the Isabelle path, or actual" |
33 echo " These are either names to be searched in the Isabelle path, or actual" |
34 echo " file names (then containing at least one /)." |
34 echo " file names (containing at least one /)." |
35 echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system." |
35 echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system." |
36 echo |
36 echo |
37 exit 1 |
37 exit 1 |
38 } |
38 } |
39 |
39 |