--- a/bin/isabelle-process Mon Oct 09 19:37:07 2006 +0200
+++ b/bin/isabelle-process Mon Oct 09 20:12:42 2006 +0200
@@ -30,7 +30,7 @@
echo " -C tell ML system to copy output image"
echo " -I startup Isar interaction mode"
echo " -P startup Proof General interaction mode"
- echo " -S secure mode -- disallow critical operations (e.g. ML evaluation)"
+ echo " -S secure mode -- disallow critical operations"
echo " -X startup PGIP interaction mode"
echo " -c tell ML system to compress output image"
echo " -e MLTEXT pass MLTEXT to the ML session"
--- a/doc-src/IsarImplementation/Thy/document/logic.tex Mon Oct 09 19:37:07 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Mon Oct 09 20:12:42 2006 +0200
@@ -775,6 +775,12 @@
}
\isamarkuptrue%
%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
+\isatagFIXME
+%
\begin{isamarkuptext}%
FIXME
@@ -857,6 +863,13 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\endisatagFIXME
+{\isafoldFIXME}%
+%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/IsarImplementation/Thy/logic.thy Mon Oct 09 19:37:07 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy Mon Oct 09 20:12:42 2006 +0200
@@ -766,7 +766,7 @@
section {* Rules \label{sec:rules} *}
-text {*
+text %FIXME {*
FIXME