# HG changeset patch
# User wenzelm
# Date 974926024 -3600
# Node ID d34192966cd8445fed68ba575a7407a8b5160390
# Parent  efb3428c98794c1b11638f15a2ec398a89ba90e8
tuned;

diff -r efb3428c9879 -r d34192966cd8 doc-src/TutorialI/Inductive/document/AB.tex
--- a/doc-src/TutorialI/Inductive/document/AB.tex	Wed Nov 22 21:41:39 2000 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Wed Nov 22 21:47:04 2000 +0100
@@ -96,7 +96,7 @@
 1 on our way from 0 to 2. Formally, we appeal to the following discrete
 intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
 \begin{isabelle}%
-\ \ \ \ \ {\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
+\ \ \ \ \ {\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
 \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
 \end{isabelle}
 where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
diff -r efb3428c9879 -r d34192966cd8 lib/scripts/feeder
--- a/lib/scripts/feeder	Wed Nov 22 21:41:39 2000 +0100
+++ b/lib/scripts/feeder	Wed Nov 22 21:47:04 2000 +0100
@@ -9,8 +9,8 @@
 
 ## diagnostics
 
-PRG=$(basename "$0")
-DIR=$(dirname "$0")
+PRG="$(basename "$0")"
+DIR="$(dirname "$0")"
 
 function usage()
 {
diff -r efb3428c9879 -r d34192966cd8 lib/scripts/isa-emacs
--- a/lib/scripts/isa-emacs	Wed Nov 22 21:41:39 2000 +0100
+++ b/lib/scripts/isa-emacs	Wed Nov 22 21:47:04 2000 +0100
@@ -9,7 +9,7 @@
 
 ## diagnostics
 
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
 
 function usage()
 {
@@ -84,13 +84,13 @@
 [ "$INITFILE" = false ] && ARGS="$ARGS -q"
 
 
-ARGS="$ARGS -l $ISAMODE_HOME/elisp/isa-site.el"
+ARGS="$ARGS -l '$ISAMODE_HOME/elisp/isa-site.el'"
 
 for FILE in "$ISABELLE_HOME/etc/isa-settings.el" \
     "$ISABELLE_HOME_USER/etc/isa-settings.el"
 do
-  [ -f "$FILE" ] && ARGS="$ARGS -l $FILE"
+  [ -f "$FILE" ] && ARGS="$ARGS -l '$FILE'"
 done
 
 ARGS="$ARGS -f isabelle"
-exec $PROGNAME -T "Isabelle" $ARGS
+eval exec "$PROGNAME" -T "Isabelle" "$ARGS"
diff -r efb3428c9879 -r d34192966cd8 lib/scripts/isa-xterm
--- a/lib/scripts/isa-xterm	Wed Nov 22 21:41:39 2000 +0100
+++ b/lib/scripts/isa-xterm	Wed Nov 22 21:47:04 2000 +0100
@@ -9,7 +9,7 @@
 
 ## diagnostics
 
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
 
 function usage()
 {
diff -r efb3428c9879 -r d34192966cd8 lib/scripts/patch-scripts.bash
--- a/lib/scripts/patch-scripts.bash	Wed Nov 22 21:41:39 2000 +0100
+++ b/lib/scripts/patch-scripts.bash	Wed Nov 22 21:47:04 2000 +0100
@@ -1,4 +1,4 @@
-#
+# -*- shell-script -*-
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
 # License: GPL (GNU GENERAL PUBLIC LICENSE)
diff -r efb3428c9879 -r d34192966cd8 src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Wed Nov 22 21:41:39 2000 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Wed Nov 22 21:47:04 2000 +0100
@@ -131,9 +131,9 @@
 
 theorem prefix_cases:
   "(xs \<le> ys ==> C) ==>
-    (ys \<le> xs ==> C) ==>
+    (ys < xs ==> C) ==>
     (xs \<parallel> ys ==> C) ==> C"
-  by (unfold parallel_def) blast
+  by (unfold parallel_def strict_prefix_def) blast
 
 theorem parallel_decomp:
   "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
@@ -164,7 +164,7 @@
       ultimately show ?thesis by blast
     qed
   next
-    assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp
+    assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
     with asm have False by blast
     thus ?thesis ..
   next