tuned;
authorwenzelm
Wed Nov 22 21:47:04 2000 +0100 (2000-11-22)
changeset 10512d34192966cd8
parent 10511 efb3428c9879
child 10513 6be063dec835
tuned;
doc-src/TutorialI/Inductive/document/AB.tex
lib/scripts/feeder
lib/scripts/isa-emacs
lib/scripts/isa-xterm
lib/scripts/patch-scripts.bash
src/HOL/Library/List_Prefix.thy
     1.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex	Wed Nov 22 21:41:39 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex	Wed Nov 22 21:47:04 2000 +0100
     1.3 @@ -96,7 +96,7 @@
     1.4  1 on our way from 0 to 2. Formally, we appeal to the following discrete
     1.5  intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
     1.6  \begin{isabelle}%
     1.7 -\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ abs\ {\isacharparenleft}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isacharparenright}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline
     1.8 +\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline
     1.9  \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
    1.10  \end{isabelle}
    1.11  where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
     2.1 --- a/lib/scripts/feeder	Wed Nov 22 21:41:39 2000 +0100
     2.2 +++ b/lib/scripts/feeder	Wed Nov 22 21:47:04 2000 +0100
     2.3 @@ -9,8 +9,8 @@
     2.4  
     2.5  ## diagnostics
     2.6  
     2.7 -PRG=$(basename "$0")
     2.8 -DIR=$(dirname "$0")
     2.9 +PRG="$(basename "$0")"
    2.10 +DIR="$(dirname "$0")"
    2.11  
    2.12  function usage()
    2.13  {
     3.1 --- a/lib/scripts/isa-emacs	Wed Nov 22 21:41:39 2000 +0100
     3.2 +++ b/lib/scripts/isa-emacs	Wed Nov 22 21:47:04 2000 +0100
     3.3 @@ -9,7 +9,7 @@
     3.4  
     3.5  ## diagnostics
     3.6  
     3.7 -PRG=$(basename "$0")
     3.8 +PRG="$(basename "$0")"
     3.9  
    3.10  function usage()
    3.11  {
    3.12 @@ -84,13 +84,13 @@
    3.13  [ "$INITFILE" = false ] && ARGS="$ARGS -q"
    3.14  
    3.15  
    3.16 -ARGS="$ARGS -l $ISAMODE_HOME/elisp/isa-site.el"
    3.17 +ARGS="$ARGS -l '$ISAMODE_HOME/elisp/isa-site.el'"
    3.18  
    3.19  for FILE in "$ISABELLE_HOME/etc/isa-settings.el" \
    3.20      "$ISABELLE_HOME_USER/etc/isa-settings.el"
    3.21  do
    3.22 -  [ -f "$FILE" ] && ARGS="$ARGS -l $FILE"
    3.23 +  [ -f "$FILE" ] && ARGS="$ARGS -l '$FILE'"
    3.24  done
    3.25  
    3.26  ARGS="$ARGS -f isabelle"
    3.27 -exec $PROGNAME -T "Isabelle" $ARGS
    3.28 +eval exec "$PROGNAME" -T "Isabelle" "$ARGS"
     4.1 --- a/lib/scripts/isa-xterm	Wed Nov 22 21:41:39 2000 +0100
     4.2 +++ b/lib/scripts/isa-xterm	Wed Nov 22 21:47:04 2000 +0100
     4.3 @@ -9,7 +9,7 @@
     4.4  
     4.5  ## diagnostics
     4.6  
     4.7 -PRG=$(basename "$0")
     4.8 +PRG="$(basename "$0")"
     4.9  
    4.10  function usage()
    4.11  {
     5.1 --- a/lib/scripts/patch-scripts.bash	Wed Nov 22 21:41:39 2000 +0100
     5.2 +++ b/lib/scripts/patch-scripts.bash	Wed Nov 22 21:47:04 2000 +0100
     5.3 @@ -1,4 +1,4 @@
     5.4 -#
     5.5 +# -*- shell-script -*-
     5.6  # $Id$
     5.7  # Author: Markus Wenzel, TU Muenchen
     5.8  # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6.1 --- a/src/HOL/Library/List_Prefix.thy	Wed Nov 22 21:41:39 2000 +0100
     6.2 +++ b/src/HOL/Library/List_Prefix.thy	Wed Nov 22 21:47:04 2000 +0100
     6.3 @@ -131,9 +131,9 @@
     6.4  
     6.5  theorem prefix_cases:
     6.6    "(xs \<le> ys ==> C) ==>
     6.7 -    (ys \<le> xs ==> C) ==>
     6.8 +    (ys < xs ==> C) ==>
     6.9      (xs \<parallel> ys ==> C) ==> C"
    6.10 -  by (unfold parallel_def) blast
    6.11 +  by (unfold parallel_def strict_prefix_def) blast
    6.12  
    6.13  theorem parallel_decomp:
    6.14    "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
    6.15 @@ -164,7 +164,7 @@
    6.16        ultimately show ?thesis by blast
    6.17      qed
    6.18    next
    6.19 -    assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp
    6.20 +    assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
    6.21      with asm have False by blast
    6.22      thus ?thesis ..
    6.23    next