equal
deleted
inserted
replaced
23 echo |
23 echo |
24 echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]" |
24 echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]" |
25 echo |
25 echo |
26 echo " Options are:" |
26 echo " Options are:" |
27 echo " -I startup Isar interaction mode" |
27 echo " -I startup Isar interaction mode" |
28 echo " -P startup ProofGeneral interaction mode" |
28 echo " -P startup Proof General interaction mode" |
29 echo " -c tell ML system to compress output image" |
29 echo " -c tell ML system to compress output image" |
30 echo " -e MLTEXT pass MLTEXT to the ML session" |
30 echo " -e MLTEXT pass MLTEXT to the ML session" |
31 echo " -m MODE add print mode for output" |
31 echo " -m MODE add print mode for output" |
32 echo " -q non-interactive session" |
32 echo " -q non-interactive session" |
33 echo " -r open heap file read-only" |
33 echo " -r open heap file read-only" |