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 [FILES|DIRS...]" |
16 echo "Usage: isabelle $PRG [FILES|DIRS...]" |
17 echo |
17 echo |
18 echo " Recursively find .thy/.ML files, removing unreadable symbol names." |
18 echo " Recursively find .thy/.ML files, removing unreadable symbol names." |
19 echo " Note: this is an ad-hoc script; there is no systematic way to replace" |
19 echo " Note: this is an ad-hoc script; there is no systematic way to replace" |
20 echo " symbols independently of the inner syntax of a theory!" |
20 echo " symbols independently of the inner syntax of a theory!" |
21 echo |
21 echo |