--- 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,
--- 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()
{
--- 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"
--- 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()
{
--- 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)
--- 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