equal
deleted
inserted
replaced
11 { |
11 { |
12 echo |
12 echo |
13 echo "Usage: isabelle $PRG [OPTIONS] IMAGE THYNAME CMD" |
13 echo "Usage: isabelle $PRG [OPTIONS] IMAGE THYNAME CMD" |
14 echo |
14 echo |
15 echo " Options are:" |
15 echo " Options are:" |
16 echo " -q run in quick'n'dirty mode" |
16 echo " -q run in quick_and_dirty mode" |
17 echo |
17 echo |
18 echo " Issues code generation using image IMAGE," |
18 echo " Issues code generation using image IMAGE," |
19 echo " theory THYNAME," |
19 echo " theory THYNAME," |
20 echo " with Isar command 'export_code CMD'" |
20 echo " with Isar command 'export_code CMD'" |
21 echo |
21 echo |