# HG changeset patch
# User wenzelm
# Date 1160417562 -7200
# Node ID cd2a6d00ec47085e8fec7a65bda48d28600baf97
# Parent  74910a189f1ddb8a37aa52a4779e92e30d982f24
tuned;

diff -r 74910a189f1d -r cd2a6d00ec47 bin/isabelle-process
--- 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"
diff -r 74910a189f1d -r cd2a6d00ec47 doc-src/IsarImplementation/Thy/document/logic.tex
--- 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
diff -r 74910a189f1d -r cd2a6d00ec47 doc-src/IsarImplementation/Thy/logic.thy
--- 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