tuned message;
authorwenzelm
Sun Aug 19 17:51:41 2012 +0200 (2012-08-19)
changeset 4885886816c61b5ca
parent 48857 9032f4bdf205
child 48859 77dd96800936
tuned message;
bin/isabelle
doc-src/System/Thy/Basics.thy
doc-src/System/Thy/document/Basics.tex
lib/scripts/tools.pl
     1.1 --- a/bin/isabelle	Sun Aug 19 17:33:00 2012 +0200
     1.2 +++ b/bin/isabelle	Sun Aug 19 17:51:41 2012 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4    echo
     1.5    echo "  Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help."
     1.6    echo
     1.7 -  echo "  Available tools are:"
     1.8 +  echo "Available tools:"
     1.9    perl -w "$ISABELLE_HOME/lib/scripts/tools.pl"
    1.10    exit 1
    1.11  }
     2.1 --- a/doc-src/System/Thy/Basics.thy	Sun Aug 19 17:33:00 2012 +0200
     2.2 +++ b/doc-src/System/Thy/Basics.thy	Sun Aug 19 17:51:41 2012 +0200
     2.3 @@ -517,10 +517,8 @@
     2.4  
     2.5    Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
     2.6  
     2.7 -  Available tools are:
     2.8 -
     2.9 -    browser - Isabelle graph browser
    2.10 -    \dots
    2.11 +Available tools:
    2.12 +  \dots
    2.13  \end{ttbox}
    2.14  
    2.15    In principle, Isabelle tools are ordinary executable scripts that
     3.1 --- a/doc-src/System/Thy/document/Basics.tex	Sun Aug 19 17:33:00 2012 +0200
     3.2 +++ b/doc-src/System/Thy/document/Basics.tex	Sun Aug 19 17:51:41 2012 +0200
     3.3 @@ -533,10 +533,8 @@
     3.4  
     3.5    Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
     3.6  
     3.7 -  Available tools are:
     3.8 -
     3.9 -    browser - Isabelle graph browser
    3.10 -    \dots
    3.11 +Available tools:
    3.12 +  \dots
    3.13  \end{ttbox}
    3.14  
    3.15    In principle, Isabelle tools are ordinary executable scripts that
     4.1 --- a/lib/scripts/tools.pl	Sun Aug 19 17:33:00 2012 +0200
     4.2 +++ b/lib/scripts/tools.pl	Sun Aug 19 17:51:41 2012 +0200
     4.3 @@ -24,7 +24,7 @@
     4.4              }
     4.5              close FILE;
     4.6              if (defined($description)) {
     4.7 -              push(@tools, "    $name - $description\n");
     4.8 +              push(@tools, "  $name - $description\n");
     4.9              }
    4.10            }
    4.11          }