equal
deleted
inserted
replaced
14 function usage() |
14 function usage() |
15 { |
15 { |
16 echo |
16 echo |
17 echo "Usage: $PRG [FILES|DIRS...]" |
17 echo "Usage: $PRG [FILES|DIRS...]" |
18 echo |
18 echo |
19 echo " Recursively find .thy and .ML files, fixing theorem names related" |
19 echo " Recursively find .thy/.ML files, fixing theorem names related" |
20 echo " to SOME (Eps) in HOL." |
20 echo " to SOME (Eps) in HOL." |
21 echo |
21 echo |
22 echo " Renames old versions of FILES by appending \"~~\"." |
22 echo " Renames old versions of FILES by appending \"~~\"." |
23 echo |
23 echo |
24 exit 1 |
24 exit 1 |
35 ## main |
35 ## main |
36 |
36 |
37 #set by configure |
37 #set by configure |
38 AUTO_PERL=perl |
38 AUTO_PERL=perl |
39 |
39 |
40 find $SPECS "(" -name \*.thy -o -name \*.ML ")" -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixsome.pl" |
40 find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \ |
|
41 xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixsome.pl" |