equal
deleted
inserted
replaced
11 PRG="$(basename "$0")" |
11 PRG="$(basename "$0")" |
12 |
12 |
13 function usage() |
13 function usage() |
14 { |
14 { |
15 echo |
15 echo |
16 echo "Usage: $PRG IMAGE THY CMD" |
16 echo "Usage: isabelle $PRG IMAGE THY CMD" |
17 echo |
17 echo |
18 echo " Issues code generation using image IMAGE," |
18 echo " Issues code generation using image IMAGE," |
19 echo " theory THY," |
19 echo " theory THY," |
20 echo " with Isar command 'export_code CMD'" |
20 echo " with Isar command 'export_code CMD'" |
21 echo |
21 echo |